@proceedings(DBLP:conf/types/1993,
 editor       = "H. Barendregt and T. Nipkow",
 year         = "1994",
 title        = "Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "806",
 publisher    = "Springer",
)
@proceedings(DBLP:conf/types/1995,
 editor       = "S. Berardi and M. Coppo",
 year         = "1996",
 title        = "Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "1158",
 publisher    = "Springer",
)
@book(bertot:book,
 author       = "Y. Bertot and P. Cast{\'e}ran",
 year         = "2004",
 title        = "Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions",
 publisher    = "Springer-Verlag",
)
@proceedings(DBLP:conf/tphol/1999,
 editor       = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
 year         = "1999",
 title        = "Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "1690",
 publisher    = "Springer",
)
@inproceedings(bertot:reccorec,
 author       = "Y. Bertot and E. Komendantskaya",
 year         = "2009",
 title        = "Using Structural Recursion for Corecursion",
 editor       = "S. Berardi and F. Damiani and U de'Liguoro",
 booktitle    = "Types for proofs and programs 2008",
 series       = "Lecture Notes in Computer Science",
 volume       = "5497",
 publisher    = "Springer",
 pages        = "220--236",
 url          = "http://hal.inria.fr/inria-00322331",
)
@inproceedings(chlipala07,
 author       = "A. Chlipala",
 year         = "2007",
 title        = "A certified type-preserving compiler from lambda calculus to assembly language",
 editor       = "Ferrante and McKinley",
 pages        = "54--65",
 url          = "http://doi.acm.org/10.1145/1250734.1250742",
)
@misc(alberto:url,
 author       = "A. Ciaffaglione",
 year         = "2011",
 title        = "The Web Appendix of this paper",
 url          = "http://www.dimi.uniud.it/ciaffagl",
)
@inproceedings(coquand93,
 author       = "T. Coquand",
 year         = "1993",
 title        = "Infinite Objects in Type Theory",
 editor       = "Barendregt and Nipkow",
 pages        = "62--78",
 url          = "http://dx.doi.org/10.1007/3-540-58085-9_72",
)
@article(coupet03,
 author       = "S. Coupet-Grimal",
 year         = "2003",
 title        = "An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions",
 journal      = "J. Log. Comput.",
 volume       = "13",
 number       = "6",
 pages        = "801--813",
 url          = "http://dx.doi.org/10.1093/logcom/13.6.801",
)
@inproceedings(coupet-jacubiec99,
 author       = "S. Coupet-Grimal and L. Jakubiec",
 year         = "1999",
 title        = "Hardware Verification Using Co-induction in COQ",
 editor       = "\write \rebib { editor = "Bertot",}",
 pages        = "91--108",
 url          = "http://dx.doi.org/10.1007/3-540-48256-3_7",
)
@inproceedings(crary03,
 author       = "K. Crary",
 year         = "2003",
 title        = "Toward a foundational typed assembly language",
 booktitle    = "POPL",
 pages        = "198--212",
 url          = "http://doi.acm.org/10.1145/640128.604149",
)
@book(cutland,
 author       = "N. J. Cutland",
 year         = "1980",
 title        = "Computability: An Introduction to Recursive Function Theory",
 publisher    = "Cambridge University Press",
)
@proceedings(DBLP:conf/types/1994,
 editor       = "P. Dybjer and B. Nordstr{\"o}m and J. M. Smith",
 year         = "1995",
 title        = "Types for Proofs and Programs, International Workshop TYPES'94, B{\r a}stad, Sweden, June 6-10, 1994, Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "996",
 publisher    = "Springer",
)
@proceedings(DBLP:conf/pldi/2007,
 editor       = "J. Ferrante and K. S. McKinley",
 year         = "2007",
 title        = "Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007",
 publisher    = "ACM",
)
@proceedings(DBLP:conf/types/2002,
 editor       = "H. Geuvers and F. Wiedijk",
 year         = "2003",
 title        = "Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "2646",
 publisher    = "Springer",
)
@inproceedings(digianantonio-miculan02,
 author       = "P. Di Gianantonio and M. Miculan",
 year         = "2002",
 title        = "A Unifying Approach to Recursive and Co-recursive Definitions",
 editor       = "Geuvers and Wiedijk",
 pages        = "148--161",
 url          = "http://dx.doi.org/10.1007/3-540-39185-1_9",
)
@inproceedings(gimenez94,
 author       = "E. Gim{\'e}nez",
 year         = "1994",
 title        = "Codifying Guarded Definitions with Recursive Schemes",
 editor       = "\write \rebib { editor = "Dybjer",}",
 pages        = "39--59",
 url          = "http://dx.doi.org/10.1007/3-540-60579-7_3",
)
@inproceedings(gimenez95,
 author       = "E. Gim{\'e}nez",
 year         = "1995",
 title        = "An Application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol",
 editor       = "Berardi and Coppo",
 pages        = "135--152",
 url          = "http://dx.doi.org/10.1007/3-540-61780-9_67",
)
@inproceedings(gimenez98,
 author       = "E. Gim{\'e}nez",
 year         = "1998",
 title        = "Structural Recursive Definitions in Type Theory",
 editor       = "\write \rebib { editor = "Larsen",}",
 pages        = "397--408",
 url          = "http://dx.doi.org/10.1007/BFb0055070",
)
@article(pi01,
 author       = "F. Honsell and M. Miculan and I. Scagnetto",
 year         = "2001",
 title        = "pi-calculus in (Co)inductive-type theory",
 journal      = "Theor. Comput. Sci.",
 volume       = "253",
 number       = "2",
 pages        = "239--285",
 url          = "http://dx.doi.org/10.1016/S0304-3975(00)00095-5",
)
@proceedings(DBLP:conf/icalp/1998,
 editor       = "K. Guldstrand Larsen and S. Skyum and G. Winskel",
 year         = "1998",
 title        = "Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "1443",
 publisher    = "Springer",
)
@article(leroy-grall09,
 author       = "X. Leroy and Herv{\'e} Grall",
 year         = "2009",
 title        = "Coinductive big-step operational semantics",
 journal      = "Inf. Comput.",
 volume       = "207",
 number       = "2",
 pages        = "284--304",
 url          = "http://dx.doi.org/10.1016/j.ic.2007.12.004",
)
@article(urm63,
 author       = "J. C. Shepherdson and H. E. Sturgis",
 year         = "1963",
 title        = "Computability of Recursive Functions",
 journal      = "J. ACM",
 volume       = "10",
 number       = "2",
 pages        = "217--255",
 url          = "http://doi.acm.org/10.1145/321160.321170",
)
@proceedings(DBLP:conf/vmcai/2004,
 editor       = "B. Steffen and G. Levi",
 year         = "2004",
 title        = "Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "2937",
 publisher    = "Springer",
)
@inproceedings(tan-appel04,
 author       = "G. Tan and A. W. Appel and K. N. Swadi and D. Wu",
 year         = "2004",
 title        = "Construction of a Semantic Model for a Typed Assembly Language",
 editor       = "Steffen and Levi",
 pages        = "30--43",
 url          = "http://dx.doi.org/10.1007/978-3-540-24622-0_4",
)
@manual(coq,
 author       = "The Coq Development Team",
 year         = "2010",
 title        = "The Coq Proof Assitant Reference Manual, version 8.3",
 organization = "INRIA",
)