Zobrazeno 1 - 2
of 2
pro vyhledávání: '"Pujet, Loïc"'
We present an extensive mechanization of the meta-theory of Martin-L\"of Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show not only the decidability of conversion, but also the decidability of
Externí odkaz:
http://arxiv.org/abs/2310.06376
Autor:
Pujet, Loïc
Publikováno v:
Logic in Computer Science [cs.LO]. Nantes Université, 2022. English. ⟨NNT : ⟩
In this thesis, I study several possibilities to extend intuitionistic type theory with extensionality principles, such as function extensionality or Voevodsky's univalence axiom, while preserving the computational properties of the proofs. In the fi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::3e075178520b2101cf849fc7dab6e906
https://hal.science/tel-03923041
https://hal.science/tel-03923041