H. Barendregt & T. Nipkow (1994):
Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers.
Lecture Notes in Computer Science 806.
Springer.
S. Berardi & M. Coppo (1996):
Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers.
Lecture Notes in Computer Science 1158.
Springer.
Y. Bertot & P. Castéran (2004):
Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions.
Springer-Verlag.
Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin & L. Théry (1999):
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings.
Lecture Notes in Computer Science 1690.
Springer.
Y. Bertot & E. Komendantskaya (2009):
Using Structural Recursion for Corecursion.
In: S. Berardi, F. Damiani & U de'Liguoro: Types for proofs and programs 2008,
Lecture Notes in Computer Science 5497.
Springer,
pp. 220–236.
Available at http://hal.inria.fr/inria-00322331.
A. Chlipala (2007):
A certified type-preserving compiler from lambda calculus to assembly language.
In: Ferrante & McKinley,
pp. 54–65.
Available at http://doi.acm.org/10.1145/1250734.1250742.
S. Coupet-Grimal (2003):
An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions.
J. Log. Comput. 13(6),
pp. 801–813.
Available at http://dx.doi.org/10.1093/logcom/13.6.801.
S. Coupet-Grimal & L. Jakubiec (1999):
Hardware Verification Using Co-induction in COQ.
In: editor = "Bertot",,
pp. 91–108.
Available at http://dx.doi.org/10.1007/3-540-48256-3_7.
N. J. Cutland (1980):
Computability: An Introduction to Recursive Function Theory.
Cambridge University Press.
P. Dybjer, B. Nordström & J. M. Smith (1995):
Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers.
Lecture Notes in Computer Science 996.
Springer.
J. Ferrante & K. S. McKinley (2007):
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007.
ACM.
H. Geuvers & F. Wiedijk (2003):
Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers.
Lecture Notes in Computer Science 2646.
Springer.
P. Di Gianantonio & M. Miculan (2002):
A Unifying Approach to Recursive and Co-recursive Definitions.
In: Geuvers & Wiedijk,
pp. 148–161.
Available at http://dx.doi.org/10.1007/3-540-39185-1_9.
E. Giménez (1995):
An Application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol.
In: Berardi & Coppo,
pp. 135–152.
Available at http://dx.doi.org/10.1007/3-540-61780-9_67.
E. Giménez (1998):
Structural Recursive Definitions in Type Theory.
In: editor = "Larsen",,
pp. 397–408.
Available at http://dx.doi.org/10.1007/BFb0055070.
F. Honsell, M. Miculan & I. Scagnetto (2001):
pi-calculus in (Co)inductive-type theory.
Theor. Comput. Sci. 253(2),
pp. 239–285.
Available at http://dx.doi.org/10.1016/S0304-3975(00)00095-5.
K. Guldstrand Larsen, S. Skyum & G. Winskel (1998):
Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings.
Lecture Notes in Computer Science 1443.
Springer.
J. C. Shepherdson & H. E. Sturgis (1963):
Computability of Recursive Functions.
J. ACM 10(2),
pp. 217–255.
Available at http://doi.acm.org/10.1145/321160.321170.
B. Steffen & G. Levi (2004):
Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings.
Lecture Notes in Computer Science 2937.
Springer.
G. Tan, A. W. Appel, K. N. Swadi & D. Wu (2004):
Construction of a Semantic Model for a Typed Assembly Language.
In: Steffen & Levi,
pp. 30–43.
Available at http://dx.doi.org/10.1007/978-3-540-24622-0_4.
The Coq Development Team (2010):
The Coq Proof Assitant Reference Manual, version 8.3.
INRIA.