By induction on the constructions of ,
Semi-continuous sized types and termination, Logical Methods in Computer Science, vol.4, issue.2, 2008. ,
DOI : 10.2168/lmcs-4(2:3)2008
URL : http://arxiv.org/abs/0804.0876
Integrating sized and dependent types, Workshop on Partiality And Recursion in Interative Theorem Provers, 2010. ,
An Introduction to Inductive Definitions, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pp.739-782, 1977. ,
DOI : 10.1016/S0049-237X(08)71120-0
On Relating Type Theories and Set Theories, Types for Proofs and Programs, International Workshop TYPES '98, pp.1-18, 1998. ,
DOI : 10.1007/3-540-48167-2_1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2658
Pure type systems with judgemental equality, Journal of Functional Programming, vol.16, issue.02, pp.219-246, 2006. ,
DOI : 10.1017/S0956796805005770
Constructions, Inductive Types and Strong Normalization, 1993. ,
Why dependent types matter . Manuscript, available online, 2005. ,
Held as Part of the Joint European Conferences on Theory and Practice of Software, 11th International Conference Proceedings, volume 4962 of Lecture Notes in Computer Science, 2008. ,
Cayenne -a language with dependent types, Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, ICFP '98, pp.239-250, 1998. ,
Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992. ,
DOI : 10.1017/cbo9781139032636
Auto-validation d'un système de preuves avec familles inductives, Thèse de doctorat, 1999. ,
Sets in Coq, Coq in sets, 1st Coq Workshop, 2009. ,
The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Amadio [9], pp.365-379 ,
DOI : 10.1007/978-3-540-78499-9_26
URL : https://hal.archives-ouvertes.fr/inria-00429543
A New Elimination Rule for the Calculus of Inductive Constructions, Berardi et al. [22], pp.32-48 ,
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00524938
Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004. ,
DOI : 10.1017/S0960129503004122
Practical Inference for Type-Based Termination in a Polymorphic Setting, Typed Lambda Calculi and Applications, 7th International Conference Proceedings, pp.71-85, 2005. ,
DOI : 10.1007/11417170_7
CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions, Hermann and Voronkov [46], pp.257-271 ,
DOI : 10.1007/11916277_18
A Tutorial on Type-Based Termination, Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, pp.100-152, 2008. ,
DOI : 10.1023/A:1019916231463
Type-Based Termination with Sized Products, Computer Science Logic, 22nd International Workshop 17th Annual Conference of the EACSL, pp.493-507, 2008. ,
DOI : 10.1007/978-3-540-87531-4_35
Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
Using Structural Recursion for Corecursion, Berardi et al. [22], pp.220-236 ,
DOI : 10.1007/BFb0105417
URL : https://hal.archives-ouvertes.fr/inria-00322331
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, Rewriting Techniques and Applications, 15th International Conference Proceedings, pp.24-39, 2004. ,
DOI : 10.1007/978-3-540-25979-4_2
URL : https://hal.archives-ouvertes.fr/inria-00100254
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems, Hermann and Voronkov [46], pp.105-119 ,
URL : https://hal.archives-ouvertes.fr/inria-00084837
General Recursion in Type Theory, Geuvers and Wiedijk, pp.39-58 ,
DOI : 10.1007/3-540-39185-1_3
Metamathematical investigations of a calculus of constructions, Logic and computer science, pp.91-122, 1990. ,
URL : https://hal.archives-ouvertes.fr/inria-00075471
Pattern matching with dependent types, Informal Proceedings Workshop on Types for Proofs and Programs, 1992. ,
Infinite objects in type theory, Barendregt and Nipkow [12], pp.62-78 ,
DOI : 10.1007/3-540-58085-9_72
The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988. ,
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024
Inductively defined types, COLOG-88, International Conference on Computer Logic Proceedings, pp.50-66, 1988. ,
DOI : 10.1007/3-540-52335-9_47
The LEGO Proof Assistant, 2001. ,
Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi, 2003. ,
Modular proof of strong normalization for the calculus of constructions, J. Funct. Program, vol.1, issue.2, pp.155-189, 1991. ,
The Netherlands, Types for Proofs and Programs, Second International Workshop, 2002. ,
Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, International Workshop TYPES'94, pp.39-59, 1994. ,
DOI : 10.1007/3-540-60579-7_3
A Calculus of Infinite Constructions and its application to the verification of communicating systems, 1996. ,
Structural recursive definitions in type theory, Automata, Languages and Programming , 25th International Colloquium, ICALP'98 BIBLIOGRAPHY Proceedings, volume 1443 of Lecture Notes in Computer Science, pp.397-408, 1998. ,
DOI : 10.1007/BFb0055070
A Typed Operational Semantics for Type Theory, 1994. ,
DOI : 10.1007/bfb0014053
Eliminating Dependent Pattern Matching, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, 2006. ,
DOI : 10.1007/11780274_27
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.7522
The Four Colour Theorem: Engineering of a Formal Proof, Computer Mathematics, 8th Asian Symposium, p.333, 2007. ,
DOI : 10.1007/978-3-540-87827-8_28
On Strong Normalization of the Calculus of Constructions with Type-Based Termination, Logic for Programming, Artificial Intelligence, and Reasoning -17th International Conference, LPAR-17 Proceedings, pp.333-347, 2010. ,
DOI : 10.1007/978-3-642-16242-8_24
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
The groupoid model refutes uniqueness of identity proofs, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.208-212, 1994. ,
DOI : 10.1109/LICS.1994.316071
Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.410-423, 1996. ,
DOI : 10.1145/237721.240882
Combinatory Reduction Systems, 1980. ,
The size-change principle for program termination, POPL, pp.81-92, 2001. ,
A proof-irrelevant model of CIC with predicative induction and judgemental equality, 2010. ,
A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009. ,
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768
Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004. ,
Basic Set Theory, 1979. ,
DOI : 10.1007/978-3-662-02308-2
A higher-order calculus and theory abstraction, Information and Computation, vol.90, issue.1, pp.107-137, 1991. ,
DOI : 10.1016/0890-5401(91)90062-7
URL : http://doi.org/10.1016/0890-5401(91)90062-7
Computation and reasoning: a type theory for computer science, 1994. ,
The Alf proof editor and its proof engine, Barendregt and Nipkow, pp.213-237 ,
DOI : 10.1007/3-540-58085-9_78
An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73, Proceedings of the Logic Colloquium of Studies in Logic and the Foundations of Mathematics, pp.73-118, 1975. ,
DOI : 10.1016/S0049-237X(08)71945-1
Dependently Typed Functional Programs and their Proofs, 1999. ,
Epigram: Practical Programming with Dependent Types, Estonia LNCS, vol.3622, 2004. ,
DOI : 10.1007/11546382_3
A Few Constructions on Constructors, Types for Proofs and Programs, pp.186-200, 2004. ,
DOI : 10.1007/11617990_12
The view from the left, Journal of Functional Programming, vol.14, issue.1, pp.69-111, 2004. ,
DOI : 10.1017/S0956796803004829
A generic normalisation proof for pure type systems, Types for Proofs and Programs, International Workshop TYPES'96, pp.254-276, 1996. ,
Inductive types and type constraints in the second-order lambda calculus, Ann. Pure Appl. Logic, vol.51, issue.12, pp.159-172, 1991. ,
Le calcul des constructions implicite: syntaxe et sémantique, 2001. ,
The Not So Simple Proof-Irrelevant Model of CC, Geuvers and Wiedijk [37], pp.240-258 ,
DOI : 10.1007/3-540-39185-1_14
Erasure and Polymorphism in Pure Type Systems, Amadio [9], pp.350-364 ,
DOI : 10.1007/978-3-540-78499-9_25
Programming in Martin-Löf 's Type Theory. An Introduction, 1990. ,
Towards a practical programming language based on dependent type theory, 2007. ,
Pattern matching coverage checking with dependent types using set approximations, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.47-56, 2007. ,
DOI : 10.1145/1292597.1292606
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.175.8980
Types for Crash Prevention, 2000. ,
Définitions Inductives en Théorie des Types d'Ordre Supérieur. HabilitationàHabilitationà diriger les recherches, 1996. ,
Polymorphism is not set-theoretic, Semantics of Data Types, International Symposium Proceedings, pp.145-156, 1984. ,
Programming in Omega, Central European Functional Programming School, Second Summer School Lecture Notes in Computer Science, vol.5161, pp.158-227, 2007. ,
Equality Is Typable in Semi-full Pure Type Systems, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.11-14, 2010. ,
DOI : 10.1109/LICS.2010.19
URL : https://hal.archives-ouvertes.fr/inria-00496988
Pure Type System conversion is always typable, Journal of Functional Programming, vol.1, issue.02, 2010. ,
DOI : 10.1017/S0956796805005770
URL : https://hal.archives-ouvertes.fr/inria-00497177
Subset Coercions in Coq, Types for Proofs and Programs, pp.237-252, 2006. ,
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869
Equations: A Dependent Pattern-Matching Compiler, Interactive Theorem Proving, First International Conference Proceedings, pp.419-434, 2010. ,
DOI : 10.1007/978-3-642-14052-5_29
URL : https://hal.archives-ouvertes.fr/inria-00628862
Verified programming in Guru, Proceedings of the 3rd workshop on Programming languages meets program verification, PLPV '09, pp.49-58, 2009. ,
DOI : 10.1145/1481848.1481856
Typing in pure type systems, Inf. Comput, vol.105, issue.1, pp.30-41, 1993. ,
Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion, 2007. ,
Sets in types, types in sets, Theoretical Aspects of Computer Software, Third International Symposium, TACS '97 Proceedings, volume 1281 of Lecture Notes in Computer Science, pp.530-346, 1997. ,
DOI : 10.1007/BFb0014566
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709
On the strength of proof-irrelevant type theories, Logical Methods in Computer Science, vol.4, issue.3, 2008. ,
Dependent Types for Program Termination Verification, Higher-Order and Symbolic Computation, vol.15, issue.1, pp.91-131, 2002. ,
DOI : 10.1023/A:1019916231463
Applied Type System (extended abstract), Post-Workshop Proceedings of TYPES 2003, pp.394-408, 2004. ,