Abstract

Temporal Type Theory (TTT) has been recently introduced as a topos-theoretic approach to understanding the behaviour of systems over time. A truly innovative point of TTT is that it makes truth inherently dependent on time; this is to be contrasted with the classical approach in which past, present and future are related via logical operators. Further on this line of research, the notion of truth is substituted by the ‘time duration’ over which a proposition is true, giving rise to the logic of temporal landscapes. In this paper, we embed 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 centred around the notion of time granularity) 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. In that respect, the addition of calendar types genuinely adds to the range of Temporal Type Theory as a powerful specification language.