Mixed Inductive/Coinductive Types and Strong Normalization, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007 Proceedings. Lecture Notes in Computer Science, p.pp, 2007. ,
DOI : 10.1007/978-3-540-76637-7_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.3001
Semi-continuous sized types and termination, Logical Methods in Computer Science, vol.42, issue.3, pp.1-33, 2008. ,
DOI : 10.2168/lmcs-4(2:3)2008
URL : http://arxiv.org/abs/0804.0876
Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types A predicative analysis of structural recursion, Proceedings of the 8th Workshop on Fixed Points in Computer Science Electronic Proceedings in Theoretical Computer Science, pp.1-11, 2002. ,
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP 2014 Electronic Proceedings in Theoretical Computer Science, pp.51-67, 2014. ,
DOI : 10.4204/EPTCS.153.4
Wellfounded recursion with copatterns: A unified approach to termination and productivity, Proceedings of the Eighteenth ACM SIG- PLAN International Conference on Functional Programming, ICFP'13, pp.185-196, 2013. ,
Analysis of a guard condition in type theory, First International Conference, FoSSaCS'98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98 Talk at the Journée " ´ egalité et terminaison " du 2 février 2010 in conjunction with JFLA 2010, pp.48-62, 1998. ,
DOI : 10.1007/BFb0053541
URL : https://hal.archives-ouvertes.fr/inria-00073388
Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004. ,
DOI : 10.1017/S0960129503004122
Size-change termination with difference constraints, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, 2008. ,
DOI : 10.1145/1353445.1353450
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.298.2757
Foundational extensible corecursion: a proof assistant perspective, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp.192-204, 2015. ,
DOI : 10.1145/2858949.2784732
URL : https://hal.archives-ouvertes.fr/hal-01212589
Infinite objects in type theory, Lecture Notes in Computer Science, vol.806, pp.62-78, 1994. ,
DOI : 10.1007/3-540-58085-9_72
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.3075
Subtyping, Declaratively, 10th International Conference, pp.100-118, 2010. ,
DOI : 10.1007/978-3-642-13321-3_8
Codifying guarded definitions with recursive schemes, Lecture Notes in Computer Science, vol.996, pp.39-59, 1994. ,
DOI : 10.1007/3-540-60579-7_3
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
The power of parameterization in coinductive proof, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, pp.193-206, 2013. ,
The size-change termination principle for constructor based languages, Logical Methods in Computer Science, vol.10, issue.11, pp.11-2014, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00547440
Infinite objects in type theory, Proceedings , Symposium on Logic in Computer Science, pp.16-18, 1986. ,
Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.159-172, 1991. ,
DOI : 10.1016/0168-0072(91)90069-X
URL : http://doi.org/10.1016/0168-0072(91)90069-x
Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction, Proceedings Seventh Workshop on Structural Operational Semantics Electronic Proceedings in Theoretical Computer Science, pp.57-75, 2010. ,
DOI : 10.4204/EPTCS.32.5
Programming in Martin Löf's Type Theory: An Introduction, 1990. ,
Inductive definitions in the system Coq rules and properties, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, pp.328-345, 1993. ,
DOI : 10.1007/BFb0037116
Enhancements of the bisimulation proof method Advanced Topics in Bisimulation and Coinduction, 2012. ,
Coq: Type-based termination in the Coq proof assistant (2015), project description ,
Type-Based Productivity of Stream Definitions in the Calculus of Constructions, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.233-242, 2013. ,
DOI : 10.1109/LICS.2013.29
On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the ??Calculus, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, pp.425-4403, 2003. ,
DOI : 10.1007/3-540-36576-1_27