Email Gateway (Aug 22 2022 at 16:22): Email Gateway (Aug 22 2022 at 16:22):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
there is a new book on encoding temporal logic in type theory:
Temporal Type Theory: A topos-theoretic approach to systems and behavior
Patrick Schultz, David I. Spivak
https://arxiv.org/abs/1710.10258
they write:
The logic we present is higher-order logic, plus subtypes and quotient
types. Higherorder
logic-aswell as its strong connectionwith topos theory-has been
verywell-studied
[LS88; Fou77; BJ81; Awo16; Joh02], which is part of our motivation for using
it. In fact,
toposes support not just higher-order logic, but also dependent type
theories. This means
that one can use an automated proof-assistant based on dependent type
theory-such as
Coq or Lean [CH88; Mou+15]-to validate proofs.
The category theory development in Isabelle I know is
https://www.isa-afp.org/entries/Category2.html
it uses the HOLZF theory.
Would encoding the above type theory in Isabelle/HOL be doable, or dependent
types are essential for that?
Last updated: Apr 26 2024 at 20:16 UTC