Tags:calendar type, Temporal Type Theory and time granularities
Abstract:
Temporal Type Theory (TTT) has been recently introduced as a topos-theoretic approach to understanding the behaviour of systems over time. In this presentation, we show how the main notions of the Calendar and Time Type System (a framework that was built for reasoning about calendric notions in the context of the Web and is centered around the notion of time granularity) can be 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 provide examples on how calendar types can be combined with temporal operators of TTT to augment the expressive power of this framework.
Embedding the Calendar and Time Type System in Temporal Type Theory