• Patrick Schultz
  • David I. Spivak
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 29)


As mentioned in the introduction, we believe that our temporal type theory can serve as a “big tent” into which to embed many disparate formalisms for proving property of behaviors. In this chapter we discuss a few of these, including hybrid dynamical systems in Sect. 8.1 , delays in Sect. 8.2 , differential equations in Sect. 8.3 , and labeled transition systems in Sect. 8.4.4 . This last occurs in Sect. 8.4 where we briefly discuss a general framework on machines, systems, and behavior contracts. Next in Sect. 8.5 we give a toy example—an extreme simplification of the National Airspace System—and prove a safety property. The idea is to show that we really can mix continuous, discrete, and delay properties without ever leaving the temporal type theory. We conclude this chapter by discussing how some temporal logics, e.g., metric temporal logic, embeds into the temporal type theory.


  1. [HOW13]
    Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 349–357. IEEE Computer Society (2013)Google Scholar
  2. [SVS16]
    Spivak, D.I., Vasilakopoulou, C., Schultz, P.: Dynamical Systems and Sheaves (2016). eprint: arXiv:1609.08086Google Scholar

Copyright information

© The Author(s) 2019

Authors and Affiliations

  • Patrick Schultz
    • 1
  • David I. Spivak
    • 1
  1. 1.Massachusetts Institute of TechnologyCambridgeUSA

Personalised recommendations