Publications

Topos semantics for a higher-order temporal logic of actions

Johnson-Freyd, Philip A.; Aytac, Jon M.; Hulette, Geoffrey

TLA is a popular temporal logic for writing stuttering-invariant specifications of digital systems. However, TLA lacks higher-order features useful for specifying modern software written in higherorder programming languages.We use categorical techniques to recast a real-time semantics for TLA in terms of the actions of a group of time dilations, or "stutters, "and an extension by a monoid incorporating delays, or "falters."Via the geometric morphism of the associated presheaf topoi induced by the inclusion of stutters into falters, we construct the first model of a higher-order TLA.