Topos Semantics for a Higher-Order Temporal Logic of Actions

Philip Johnson-Freyd
(Sandia National Laboratories)
Jon Aytac
(Sandia National Laboratories)
Geoffrey Hulette
(Sandia National Laboratories)

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 higher-order 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.

In John Baez and Bob Coecke: Proceedings Applied Category Theory 2019 (ACT 2019), University of Oxford, UK, 15-19 July 2019, Electronic Proceedings in Theoretical Computer Science 323, pp. 161–171.
Published: 15th September 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.323.11 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org