Title: Temporal Type Theory: A topos-theoretic approach to systems and behavior,
Abstract: This book introduces a temporal type theory, the first of its kind as far as
we know. It is based on a standard core, and as such it can be formalized in a
proof assistant such as Coq or Lean by adding a number of axioms. Well-known
temporal logics---such as Linear and Metric Temporal Logic (LTL and
MTL)---embed within the logic of temporal type theory.
The types in this theory represent "behavior types". The language is rich
enough to allow one to define arbitrary hybrid dynamical systems, which are
mixtures of continuous dynamics---e.g. as described by a differential
equation---and discrete jumps. In particular, the derivative of a continuous
real-valued function is internally defined.
We construct a semantics for the temporal type theory in the topos of sheaves
on a translation-invariant quotient of the standard interval domain. In fact,
domain theory plays a recurring role in both the semantics and the type theory.