modal logic & temporal type theory

Stream: Lean Together 2019

[Joseph Corneli]

These talks reminded me of https://arxiv.org/abs/1710.10258

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.

[Simon Hudon]

Nice! Thanks!