Embedding the Calendar and Time Type System in Temporal Type Theory
Temporal Type Theory, a member of the family of Martin-Löf style type
theories, has been recently introduced as a topos-theoretic approach to
understanding the behaviour of systems over time. We describe how the
main notions of the Calendar and Time Type System were embedded in
Temporal Type Theory, attempting to address a common requirement in the
practical use of temporal formalisms: the ability to speak about certain
time moments and appropriate time windows in (past and future) time, in
the form of hours, dates, holidays, etc. With a view to concrete
applications, we then provide examples on how calendar types can be
combined with elements of Temporal Type Theory to augment its expressive
power, placing special emphasis on capturing crucial temporal aspects of
business processes that stem from (smart) contracts. In that respect,
the addition of calendar types genuinely adds to the range of Temporal
Type Theory as a powerful specification language.
Georgios V. Pitsiladis
Last modified: Mon Dec 9 2024