Exploring Concepts of Interactive Theorem Proving

Abstract

This paper formally presents the Calculus of Inductive Constructions (CiC), the expressive type system behind the Coq proof assistant. We begin with a brief review of the untyped λ-calculus and progressively build the CiC framework. As a case study, we formalize in Coq the proof that is a natural number for all , and relate it to its traditional counterpart. We then extract the Coq proof to Haskell, illustrating the Curry-Howard Isomorphism. The paper also examines the role of dependent types and heterogeneous equality, discusses the controlled use of axioms in dependently typed proofs, and outlines strategies for avoiding axioms to simplify reasoning. 

Keywords

• Lambda Calculus
• Pure Type Systems
• Calculus of Inductive Constructions
• Interactive Theorem Proving
• Cuury-Howard Isomorphism
• The Coq Proof Assistant

References

1. [1] The Coq Development Team, The Coq proof assistant reference manual, https://coq.inria.fr/distrib/current/refman/, 2018, version 8.8.1.
2. [2] D. Delahaye, “A tactic language for the system coq,” in Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, ser. Lecture Notes in Computer Science, M. Parigot and A. Voronkov, Eds., vol. 1955. Springer, 2000, pp. 85–95. [Online]. Available: https://doi.org/10.1007/3-540-44404-1 7
3. [3] B. Werner, “Sets in types, types in sets,” in Theoretical Aspects of Computer Software, Third International Symposium, TACS ’97, Sendai, Japan, September 23-26, 1997, Proceedings, ser. Lecture Notes in Computer Science, M. Abadi and T. Ito, Eds., vol. 1281. Springer, 1997, pp. 530–346. [Online]. Available: https://doi.org/10.1007/BFb0014566
4. [4] W. A. Howard, “The formulæ-as-types notion of construction,” in The Curry-Howard Isomorphism, P. D. Groote, Ed. Academia, 1995.
5. [5] H. Barendregt, “Lambda calculi with types,” in HANDBOOK OF LOGIC IN COMPUTER SCIENCE. Oxford University Press, 1992, pp. 117– 309.
6. [6] H. Barendregt, “Introduction to generalized type systems,” J. Funct. Program., vol. 1, no. 2, pp. 125–154, 1991.
7. [7] A. Church, “A formulation of the simple theory of types,” Journal of Symbolic Logic, vol. 5, no. 2, pp. 56–68, 06 1940. [Online]. Available: https://projecteuclid.org:443/euclid.jsl/1183387805
8. [8] J. Girard, “The system F of variable types, fifteen years later,” Theor. Comput. Sci., vol. 45, no. 2, pp. 159–192, 1986. [Online]. Available: https://doi.org/10.1016/0304-3975(86)90044-7

9. [9] T. Coquand and G. P. Huet, “The calculus of constructions,” Inf. Comput., vol. 76, no. 2/3, pp. 95–120, 1988. [Online]. Available: https://doi.org/10.1016/0890-5401(88)90005-3
10. [10] T. Coquand and C. Paulin, “Inductively defined types,” in COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, ser. Lecture Notes in Computer Science, P. Martin- L¨of and G. Mints, Eds., vol. 417. Springer, 1988, pp. 50–66. [Online]. Available: https://doi.org/10.1007/3-540-52335-9 47
11. [11] P. Letouzey, “Extraction in Coq: An Overview,” in Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings, ser. Lecture Notes in Computer Science, A. Beckmann, C. Dimitracopoulos, and B. L¨owe, Eds., vol. 5028. Springer, 2008, pp. 359–369. [Online]. Available: https://doi.org/10.1007/978-3-540-69407-6 39
12. [12] C. McBride, “Elimination with a motive,” in TYPES, ser. Lecture Notes in Computer Science, vol. 2277. Springer, 2000, pp. 197–216.