References

  1. 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.
  2. 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.
  3. Y. Bertot & P. Castéran (2004): Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag.
  4. 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.
  5. 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.
  6. 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.
  7. A. Ciaffaglione (2011): The Web Appendix of this paper. Available at http://www.dimi.uniud.it/ciaffagl.
  8. T. Coquand (1993): Infinite Objects in Type Theory. In: Barendregt & Nipkow, pp. 62–78. Available at http://dx.doi.org/10.1007/3-540-58085-9_72.
  9. 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.
  10. 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.
  11. K. Crary (2003): Toward a foundational typed assembly language. In: POPL, pp. 198–212. Available at http://doi.acm.org/10.1145/640128.604149.
  12. N. J. Cutland (1980): Computability: An Introduction to Recursive Function Theory. Cambridge University Press.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. E. Giménez (1994): Codifying Guarded Definitions with Recursive Schemes. In: editor = "Dybjer",, pp. 39–59. Available at http://dx.doi.org/10.1007/3-540-60579-7_3.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. X. Leroy & Hervé Grall (2009): Coinductive big-step operational semantics. Inf. Comput. 207(2), pp. 284–304. Available at http://dx.doi.org/10.1016/j.ic.2007.12.004.
  23. 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.
  24. 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.
  25. 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.
  26. The Coq Development Team (2010): The Coq Proof Assitant Reference Manual, version 8.3. INRIA.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org