Extensional equality in intensional type theory, 14th Symposium on Logic in Computer Science, pp.412-420, 1999. ,
Type theory in type theory using quotient inductive types, Proceedings of POPL 2016, pp.18-29, 2016. ,
,
Towards a Cubical Type Theory without an Interval, TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs), vol.69, pp.1-3, 2018. ,
Observational equality, now! In: PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification, pp.57-58, 2007. ,
Towards certified meta-programming with typed template-coq, ITP 2018-9th Conference on Interactive Theorem Proving, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01809681
A relationally parametric model of dependent type theory, Proceedings of POPL '14, pp.503-516, 2014. ,
Proofs for free -parametricity for dependent types, Journal of Functional Programming, vol.22, issue.02, pp.107-152, 2012. ,
A model of type theory in cubical sets, 19th International Conference on Types for Proofs and Programs (TYPES 2013), vol.26, pp.107-128, 2014. ,
Extending Type Theory with Syntactic Models, 2018. ,
URL : https://hal.archives-ouvertes.fr/tel-02007839
The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.182-194, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
,
Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic, vol.32, pp.209-243, 1986. ,
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom, TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs), vol.69, pp.1-5, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01378906
Internal type theory, Lecture Notes in Computer Science. pp, pp.120-134, 1996. ,
Definitional Proof-Irrelevance without K, Proceedings of POPL 2019, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01859964
Syntactic investigations into cubical type theory, TYPES 2018. University of Minho, 2018. ,
Conservativity of equality reflection over intensional type theory, TYPES 95, pp.153-164, 1995. ,
Extensional concepts in intensional type theory. Thesis, 1995. ,
Syntax and semantics of dependent types, Semantics and Logics of Computation, pp.79-130, 1997. ,
The groupoid interpretation of type theory. In: In Venice Festschrift, pp.83-111, 1996. ,
The definitional side of the forcing, Proceedings of LICS '16, pp.367-376, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01319066
The setoid model formalized in Agda, 2019. ,
Constructing quotient inductiveinductive types, Proc. ACM Program. Lang. 3(POPL), vol.2, 2019. ,
Intuitionistic type theory, Studies in Proof Theory, vol.1, 1984. ,
, , 2013.
Elimination with a motive, Selected Papers from the International Workshop on Types for Proofs and Programs, pp.197-216, 2002. ,
Extensionality in the calculus of constructions, pp.278-293, 2005. ,
Homotopy type theory: Univalent foundations of mathematics, Tech. rep., Institute for Advanced Study, 2013. ,
Cubical syntax for reflection-free extensional equality, Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), vol.131, 2019. ,
Investigations into intensional type theory, 1993. ,
Equivalences for Free, ICFP 2018 -International Conference on Functional Programming, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01559073
Engineering proof by reflection in agda, Symposium on Implementation and Application of Functional Languages, pp.157-173, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00987610
Using reflection to eliminate reflection, 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho, 2018. ,