Online ISSN:1349-8606
Progress in Informatics  
No.10 March 2013  
Page 47-63  
 
Wander types : A formalization of coinduction-recursion
Venanzio CAPRETTA

LINK [1] Y. Bertot and P. Castéran. Interactive theorem proving and program development. Coq'Art: The calculus of inductive constructions, Springer, 2004.

LINK [2] A. Bove and V. Capretta, “Nested general recursion and partiality in type theory,” In R. J. Boulton and P. B. Jackson, editors, Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, vol.2152 of Lecture Notes in Computer Science, pp.121-135, Springer-Verlag, 2001.

LINK [3] A. Bove, P. Dybjer, and U. Norell, “A brief overview of Agda-a functional language with dependent types,” In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, TPHOLs 2009, vol.5674 of Lecture Notes in Computer Science, pp.73-78, Springer, 2009.

LINK [4] T. Coquand, “Infinite objects in type theory,” In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs. International Workshop TYPES'93, vol.806 of Lecture Notes in Computer Science, pp.62-78, Springer-Verlag, 1993.

LINK [5] N. Danielsson and T. Altenkirch, “Subtyping, declaratively,” In C. Bolduc, J. Desharnais, and B. Ktari, editors, Mathematics of Program Construction (MPC 2010), vol.6120 of Lecture Notes in Computer Science, pp.100-118. Springer Berlin/Heidelberg, 2010.

LINK [6] P. Dybjer, “A general formulation of simultaneous inductive-recursive definitions in type theory,” Journal of Symbolic Logic, vol.65, no.2, 2000.

LINK [7] P. Dybjer and A. Setzer, “A finite axiomatization of inductive-recursive definitions,” In Proceedings of TLCA 1999, vol.1581 of LNCS, pp.129-146, Springer-Verlag, 1999.

LINK [8] N. Ghani and P. Hancock, “An algebraic foundation and implementation of induction recursion and indexed induction recursion,” Draft paper, 2011.

LINK [9] N. Ghani, P. Hancock, L. Malatesta, and A. Setzer, “Fibred data types,” Draft paper, 2012.

LINK [10] N. Ghani, P. Hancock, and D. Pattinson, “Continuous functions on final coalgebras,” Electr. Notes Theor. Comput. Sci., vol.164, no.1, pp.141-155, 2006. Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science (CMCS 2006).

LINK [11] N. Ghani, P. Hancock, and D. Pattinson, “Continuous functions on final coalgebras,” Electr. Notes Theor. Comput. Sci., vol.249, pp.3-18, 2009. Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009).

LINK [12] N. Ghani, P. Hancock, and D. Pattinson, “Representations of stream processors using nested fixed points,” Logical Methods in Computer Science, vol.5, no.3, 2009.

LINK [13] D. E. Knuth. The Art of Computer Programming, Volume III: Sorting and Searching. Addison-Wesley, 1973.

LINK [14] L. Malatesta, T. Altenkirch, N. Ghani, P. Hancock, and C. McBride, “Small induction recursion, indexed containers and dependent polynomials are equivalent,” Submitted for publication, 2012.

LINK [15] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.

LINK [16] P. Martin-Löf, “Mathematics of infinity,” In P. Martin-Löf and G. Mints, editors, Conference on Computer Logic, vol.417 of Lecture Notes in Computer Science, pp.146-197, Springer, 1988.

LINK [17] C. Okasaki. Purely functional data structures. Cambridge University Press, 1999.

LINK [18] E. Palmgren, “On universes in type theory,” In Giovanni Sambin and Jan Smith, editors, Twenty-Five Years of Constructive Type Theory, vol.36 of Oxford Logic Guides, pp.191-204, Oxford Science Publications, 1998. Proceedings of a Congress Held in Venice, Oct. 1995.

LINK [19] M. Rathjen, “The strength of Martin-Löf type theory with a superuniverse. Part I,” Arch. Math. Log., vol.39, no.1, pp.1-39, 2000.

LINK [20] M. Rathjen, “The strength of Martin-Löf type theory with a superuniverse. Part II,” Arch. Math. Log., vol.40, no.3, pp.207-233, 2001.

LINK [21] M. Rathjen, E. R. Griffor, and E. Palmgren, “Inaccessibility in constructive set theory and type theory,” Annals of Pure and Applied Logic, vol.94, no.1-3, pp.181-200, 1998.

LINK [22] The Coq Development Team. The Coq Proof Assistant. Reference Manual. Version 8. INRIA, 2011: http://coq.inria.fr/refman/index.html