Decidability of conversion for type theory in type theory, Proc. ACM Program. Lang. 2, POPL, Article 23, p.3158111, 2018. ,
DOI : 10.1109/LICS.2008.44
On Irrelevance and Algorithmic Equality in Predicative Type Theory, Logical Methods in Computer Science, vol.15, issue.5/6, pp.29-2012, 2012. ,
DOI : 10.2168/LMCS-4(3:13)2008
Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.412-420, 1999. ,
DOI : 10.1109/LICS.1999.782636
Extending Homotopy Type Theory with Strict Equality, CSL, 2016. ,
Propositions as [Types], Journal of Logic and Computation, vol.14, issue.4, pp.447-471, 2004. ,
DOI : 10.1093/logcom/14.4.447
The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp.182-194, 2017. ,
DOI : 10.1109/LICS.1989.39193
URL : https://hal.archives-ouvertes.fr/hal-01445835
Inductive Families Need Not Store Their Indices, Types for Proofs and Programs, pp.115-129, 2004. ,
DOI : 10.1007/978-3-540-24849-1_8
Models of type theory with strict equality, 2017. ,
Elaborating dependent (co)pattern matching, Proceedings of the 23th ACM SIGPLAN Conference on Functional Programming, 2018. ,
DOI : 10.1145/1328438.1328482
Abstract, Journal of Functional Programming, vol.28, 2018. ,
DOI : 10.1016/0890-5401(91)90066-B
Pattern matching without K, ACM SIGPLAN Notices, vol.49, issue.9, pp.257-268, 2014. ,
DOI : 10.1007/978-3-642-38946-7_14
Universe of Bishop sets, 2016. ,
Internal type theory, Types for Proofs and Programs, pp.120-134, 1996. ,
DOI : 10.1007/3-540-61780-9_66
Conservativity of equality reflection over intensional type theory, International Workshop on Types for Proofs and Programs, pp.153-164, 1995. ,
DOI : 10.1007/3-540-61780-9_68
Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004. ,
Equations Reloaded, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01671777
An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73, pp.73-118, 1975. ,
DOI : 10.1016/S0049-237X(08)71945-1
Intensionality, extensionality, and proof irrelevance in modal type theory, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, p.221, 2001. ,
DOI : 10.1109/LICS.2001.932499
, The Univalent Foundations Program Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.
Resising Rules -their use and semantic justification. www.math.ias, 2011. ,
A simple type system with two identity types, 2013. ,
On the Strength of Proof-Irrelevant Type Theories, pp.1-20, 2008. ,
Type axiom r : A ? A ? Prop ,