Stream: Lean Together 2019
Joseph Corneli (Jan 07 2019 at 16:23):
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 (Jan 07 2019 at 21:35):
Last updated: May 08 2021 at 21:09 UTC