Type-Based Termination. A Polymorphic Lambda-Calculus with Sized Higher-Order Types, 2006. ,
An Introduction to Inductive Definitions, Handbook of Mathematical Logic, pp.739-782, 1977. ,
DOI : 10.1016/S0049-237X(08)71120-0
Algebras and Coalgebras, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, pp.79-88, 2000. ,
DOI : 10.1007/3-540-47797-7_3
Fixpoint equations for well-founded recursion in type theory, Theorem Proving in Higher-Order Logics: 13th International Conference, pp.1-16, 2000. ,
Fonctions récursives générales par itération en théorie des types, Journées Francophones pour les Langages Applicatifs, 2002. ,
Lambda calculi with types, Handbook of Logic in Computer Science, volume II, pp.117-309, 1992. ,
DOI : 10.1017/cbo9781139032636
Proof-checking using dependent type systems, Handbook of Automated Reasoning, volume II, chapter 18, pp.1149-1240, 2001. ,
DOI : 10.1016/b978-044450813-3/50020-5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7813
The relevance of proof-irrelevance, Authomata, Languages and Programming (ICALP'98), pp.755-768, 1998. ,
DOI : 10.1007/BFb0055099
Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004. ,
DOI : 10.1017/S0960129503004122
Filters and co-inductive streams, an application to eratosthenes' sieve, TLCA, pp.102-115, 2005. ,
DOI : 10.1007/11417170_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.5339
Affine functions and series with co-inductive real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, pp.37-63, 2007. ,
DOI : 10.1017/S0960129506005809
URL : https://hal.archives-ouvertes.fr/inria-00001171
Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Experiments towards general co-recursion: Coq code, 2008. ,
DOI : 10.1007/978-3-662-07964-5_15
Simple general recursion in type theory, Nordic Journal of Computing, vol.8, issue.1, pp.22-42, 2001. ,
General Recursion in Type Theory, 2002. ,
DOI : 10.1007/3-540-39185-1_3
General Recursion in Type Theory, TYPES, pp.39-58, 2002. ,
DOI : 10.1007/3-540-39185-1_3
Nested General Recursion and Partiality in Type Theory, TPHOLs, pp.121-135, 2001. ,
DOI : 10.1007/3-540-44755-5_10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.1831
Modelling general recursion in type theory, Mathematical Structures in Computer Science, vol.15, issue.4, pp.671-708, 2005. ,
DOI : 10.1017/S0960129505004822
A term calculus for (co-)recursive definitions on streamlike data structures, Annals of Pure and Applied Logic, vol.136, issue.1-2, pp.75-90, 2005. ,
DOI : 10.1016/j.apal.2005.05.006
General recursion via coinductive types, Logical Methods in Computer Science, vol.1, issue.2, 2005. ,
DOI : 10.2168/LMCS-1(2:1)2005
URL : http://arxiv.org/abs/cs/0505037
Pattern-matching in type theory, Informal Proceedings of the 1992 workshop on Types for Proofs and Programs, pp.71-84, 1992. ,
Infinite objects in type theory, Types for Proofs and Programs, pp.62-78, 1994. ,
DOI : 10.1007/3-540-58085-9_72
The calculus of constructions, Information and Computation, vol.76, issue.2-3, 1988. ,
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024
On the productivity of recursive definitions, p.749, 1980. ,
A New Representation for Exact Real Numbers, MFPS XIII, 1997. ,
DOI : 10.1016/S1571-0661(05)80166-5
Productivity of stream definitions, FCT, pp.274-287, 2007. ,
DOI : 10.1016/j.tcs.2009.10.014
URL : http://doi.org/10.1016/j.tcs.2009.10.014
Logics and Type Systems, 1993. ,
A Functional Approach to Computability on Real Numbers, 1993. ,
A Unifying Approach to Recursive and Co-recursive Definitions, TYPES, pp.148-161, 2002. ,
DOI : 10.1007/3-540-39185-1_9
Unifying Recursive and Co-recursive Definitions in Sheaf Categories, FoSSaCS, pp.136-150, 2004. ,
DOI : 10.1007/978-3-540-24727-2_11
Un Calcul de Constructions Infinies et son Application a la Verification des Systemes Communcants, 1996. ,
The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980. ,
Induction principles formalised in calculus of constructions, To H.B. Curry: Essays on Combinatory Logic, Lmabda Calculus, and formalism, pp.479-490, 1988. ,
Exercises in Coalgebraic Specification, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, number 2297 in LNCS, pp.237-280, 2002. ,
DOI : 10.1007/3-540-47797-7_7
A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, pp.222-259, 1997. ,
Recursive Function Definition over Coinductive Types, TPHOLs, pp.73-90, 1999. ,
DOI : 10.1007/3-540-48256-3_6
Formalising Exact Arithmetic: Representations, Algorithms and Proofs, 2004. ,
DOI : 10.1007/11494645_46
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.6690
Coinductive Field of Exact Real Numbers and General Corecursion, Proc. of CMCS'06, pp.121-139, 2006. ,
DOI : 10.1016/j.entcs.2006.06.008
Terminating general recursion, BIT, vol.24, issue.3, pp.605-619, 1988. ,
DOI : 10.1007/BF01941137
Inductive definitions in the system Coq rules and properties, TLCA, pp.328-345, 1993. ,
DOI : 10.1007/BFb0037116
Mechanizing coinduction and corecursion in higher-order logic, Logic and Computation, pp.175-204, 1997. ,
DOI : 10.1093/logcom/7.2.175
The temporal semantics of concurrent programs, Theoretical Computer Science, issue.31, pp.45-60, 1981. ,
On the productivity of recursive list definitions, ACM Transactions on Programming Languages and Systems, vol.11, issue.4, pp.633-649, 1989. ,
DOI : 10.1145/69558.69563