A. Abel, Semi-continuous Sized Types and Termination, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, vol.4207, pp.72-88, 2006.
DOI : 10.1007/11874683_5
URL : http://arxiv.org/pdf/0804.0876v1.pdf

A. Abel and B. Pientka, Well-founded recursion with copatterns and sized types, J. Funct. Program, vol.26, 2016.

T. Altenkirch, C. Mcbride, and W. Swierstra, Observational Equality, Now!, PLPV'07, 2007.
DOI : 10.1145/1292597.1292608
URL : http://strictlypositive.org/obseqnow.pdf

A. Bove, A. Krauss, and M. Sozeau, Partiality and recursion in interactive theorem provers-an overview, Mathematical Structures in Computer Science FirstView, pp.1-51, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00691459

A. Anand, A. Appel, G. Morrisett, Z. Paraskevopoulou, R. Pollack et al., CertiCoq: A verified compiler for Coq, CoqPL, 2017.

J. Avigad, G. Ebner, and S. Ullrich, The Lean Reference Manual, 2017.

G. Barthe, J. Forest, D. Pichardie, and V. Rusu, Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. Functional and Logic Programming, pp.114-129, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00564237

A. Bauer, J. Gross, P. Lefanu-lumsdaine, M. Shulman, M. Sozeau et al., The HoTT Library: A formalization of homotopy type theory in Coq, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01421212

L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters et al., Guarded Cubical Type Theory: Path Equality for Guarded Recursion, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, vol.62, pp.1-23, 2016.
DOI : 10.1007/s10817-018-9471-7
URL : http://arxiv.org/pdf/1611.09263

J. Cockx, Dependent Pattern Matching and Proof-Relevant Unification, Ph.D. Dissertation. Katholieke Universiteit Leuven, 2017.

J. Cockx and D. Devriese, Lifting proof-relevant unification to higher dimensions, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.173-181, 2017.
DOI : 10.1145/3018610.3018612

J. Cockx, D. Devriese, and F. Piessens, Pattern matching without K, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp.257-268, 2014.
DOI : 10.1145/2628136.2628139

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01378906

. Thierry-coquand, Pattern Matching with Dependent Types, Proceedings of the Workshop on Logical Frameworks, 1992.

H. Goguen, C. Mcbride, and J. Mckinna, Eliminating Dependent Pattern Matching, Essays Dedicated to Joseph A. Goguen (Lecture Notes in Computer Science), vol.4060, pp.521-540, 2006.
DOI : 10.1007/11780274_27

M. Hofmann and T. Streicher, A Groupoid Model Refutes Uniqueness of Identity Proofs, LICS, pp.208-212, 1994.
DOI : 10.1109/lics.1994.316071

N. Kraus, M. Escardó, T. Coquand, and T. Altenkirch, Generalizations of Hedberg's Theorem, Lecture Notes in Computer Science, vol.7941, pp.173-188, 2013.
DOI : 10.1007/978-3-642-38946-7_14
URL : http://www.cs.bham.ac.uk/~mhe/papers/hedberg.pdf

S. Lescuyer, Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq, Ph.D. Dissertation. University of Paris-Sud, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

. Peter-lefanu-lumsdaine, Weak omega-categories from intensional type theory, Logical Methods in Computer Science, vol.6, p.3, 2010.

C. Mangin and M. Sozeau, Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study, Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (EPTCS), vol.185, 2015.
DOI : 10.4204/eptcs.185.5
URL : http://arxiv.org/pdf/1508.00455

P. Martin-löf, Intuitionistic type theory, Studies in Proof Theory, vol.1, 1984.

C. Mcbride, Dependently Typed Functional Programs and Their Proofs, Ph.D. Dissertation. University of Edinburgh, 1999.

C. Mcbride, .. ;. , P. Callaghan, and Z. Luo, Elimination with a Motive, TYPES (Lecture Notes in Computer Science), vol.2277, pp.197-216, 2000.

C. Mcbride, H. Goguen, and J. Mckinna, A Few Constructions on Constructors. Types for Proofs and Programs, pp.186-200, 2004.

J. Monin and X. Shi, Handcrafted Inversions Made Operational on Operational Semantics, pp.338-353, 2013.
DOI : 10.1007/978-3-642-39634-2_25
URL : https://hal.archives-ouvertes.fr/hal-00937168

U. Norell, Towards a practical programming language based on dependent type theory, 2007.

C. Paulin-mohring, Inductive Definitions in the System Coq-Rules and Properties, Typed Lambda Calculi and Applications, vol.664, pp.328-345, 1993.
DOI : 10.1007/bfb0037116

Á. Pelayo, A. Michael, and . Warren, Homotopy type theory and Voevodsky's univalent foundations, 2012.
DOI : 10.1090/s0273-0979-2014-01456-9
URL : https://www.ams.org/bull/2014-51-04/S0273-0979-2014-01456-9/S0273-0979-2014-01456-9.pdf

M. Sozeau, Program-ing Finger Trees in Coq, ICFP'07, pp.13-24, 2007.

M. Sozeau, Equations: A Dependent Pattern-Matching Compiler, First International Conference on Interactive Theorem Proving, 2010.
DOI : 10.1007/978-3-642-14052-5_29
URL : https://hal.archives-ouvertes.fr/inria-00628862

A. Spector-zabusky, J. Breitner, C. Rizkallah, and S. Weirich, Total Haskell is reasonable Coq, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.14-27, 2018.
DOI : 10.1145/3176245.3167092
URL : http://arxiv.org/pdf/1711.09286

, The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study

. Benno-van-den, R. Berg, and . Garner, Types are weak ?-groupoids, Proceedings of the London Mathematical Society, vol.102, pp.370-394, 2011.