Advertisement

Type Theories from Barendregt’s Cube for Theorem Provers

  • Jonathan P. SeldinEmail author
Chapter
Part of the Trends in Logic book series (TREN, volume 39)

Abstract

Anybody using a theorem prover or proof assistant will want to have confidence that the system involved will not permit the derivation of false results. On some occasions, there is more than the usual need for this confidence. This chapter discusses some logical systems based on typed lambda-calculus that can be used for this purpose. The systems are natural deduction systems, and use the propositions-as-types paradigm. Not only are the underlying systems provably consistent, but additional unproved assumptions from which a lot of ordinary mathematics can be derived can also be proved consistent. Finally, the systems have few primitive postulates that need to be programmed separately, so that it is easier for a programmer to see whether the code really does program the systems involved without errors.

Notes

Acknowledgments

This work was supported in part by grant RGP-23391-98 from the Natural Sciences and Engineering Research Council of Canada.

References

  1. 1.
    Appel, A. W., & Felty, A. P. (2000). A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM symposium on the principles of programming languages (pp. 243–253).Google Scholar
  2. 2.
    Appel, A. W., & McAllester, D. (2000). An indexed model of recursive types for foundational proof-carrying code. Technical report TR-629-00, Princeton University.Google Scholar
  3. 3.
    Barendregt, H. P. (1992). Lambda calculi with types. In S. Abramsky, D. M. Gabbay, & T. S. E. Maibaum (Eds.), Handbook of logic in computer science (Vol. 2, pp. 117–309). Oxford: Oxford University Press.Google Scholar
  4. 4.
    Beeson, M. (1985). Foundations of constructive mathematics. Berlin: Springer.CrossRefGoogle Scholar
  5. 5.
    Berardi, S. (1989). Type dependence and constructive mathematics. Ph.D. thesis, Universita di Torino.Google Scholar
  6. 6.
    Berardi, S. (1993). Encoding of data types in pure construction calculus: a semantic justification. In G. Huet, & G. Plotkin (Eds.), Logical Environments (pp. 30–60). Cambridge: Cambridge University Press.Google Scholar
  7. 7.
    Blanqui, F. (1998). The calculus of algebraic and inductive constructions. Technical report, DEA Sémantique, preuve et Programmation.Google Scholar
  8. 8.
    Böhm, C., & Berarducci, A. (1985). Automatic synthesis of typed \(\Lambda \)-programs on term algebras. Theoretical Computer Science, 39(2–3), 135–154.CrossRefGoogle Scholar
  9. 9.
    Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 56–68.CrossRefGoogle Scholar
  10. 10.
    Constable, R., et al. (1986). Implementing mathematics with the Nuprl proof development system. Englewood Cliffs: Prentice-Hall.Google Scholar
  11. 11.
    Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76, 95–120.CrossRefGoogle Scholar
  12. 12.
    Coquand, T., & Paulin, C. (1990). Inductively defined types. In P. Martin-Löf, & G. Mints (Eds.), COLOG-88: Proceedings of the international conference on computer logic held in Tallinn, December 12–16, 1988, Lecture notes in computer science (Vol. 417, pp. 50–66). Springer.Google Scholar
  13. 13.
    Dedekind, R. (1887). Was sind und was sollen die Zahen? (10th ed., 1965). Braunschweig: Friedr. Vieweg & Sohn.Google Scholar
  14. 14.
    Howard, W. A. (1980). The formulae-as-types notion of construction. In J. Roger Hindley & J. P. Seldin (Eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479–490). New York: Academic. A version of this paper was privately circulated in 1969.Google Scholar
  15. 15.
    Huet, G. (1986). Formal structures for computation and deduction (1st ed.). Course notes, Carnegie-Mellon University.Google Scholar
  16. 16.
    Huet, G. (1987). Induction principles formalized in the calculus of constructions. In H. Ehrig, R. Kowalski, G. Levi, & U. Montanari (Eds.), TAPSOFT ’87: Proceedings of the international joint conference on theory and practice of software development, Pisa, Italy, March 23–27, 1987. Advanced seminar on foundations of innovative software development I and colloquium on trees in algebra and programming (CAAP ’87) (Vol. 1), Lecture notes in computer science (Vol. 249, pp. 276–286). Berlin: Springer.Google Scholar
  17. 17.
    Kalmár, L. (1940). On the possibility of definition by recursion. Acta Szeged, 9(4), 227–232.Google Scholar
  18. 18.
    Lorenzen, P. (1939). Die Definition durch vollständige Induktion. Monatshefte für Mathematik und Physik, 47, 356–358.CrossRefGoogle Scholar
  19. 19.
    Pfenning, F. & Paulin-Mohring, C. (1989). Inductively defined types in the calculus of constructions. In M. Main, A. Melton, M. Mislove, & D. Schmidt (Eds.), Proceedings of the 5th international conference on mathematical foundations of programming semantics, Tulane University, New Orleans, Louisiana, USA, March 29–April 1, 1989, Lecture notes in computer science, (Vol. 442, pp. 209–228). Springer.Google Scholar
  20. 20.
    Prawitz, D. (1965). Natural deduction. Stockholm: Almqvist & Wiksell.Google Scholar
  21. 21.
    Seldin, J. P. (1992). Coquand’s calculus of constructions: a mathematical foundation for a proof development system. Formal Aspects of Computing, 4, 425–441.CrossRefGoogle Scholar
  22. 22.
    Seldin, J. P. (1997). On the proof theory of Coquand’s calculus of constructions. Annals of Pure and Applied Logic, 83, 23–101.CrossRefGoogle Scholar
  23. 23.
    Seldin, J. P. (2000). A Gentzen-style sequent calculus of constructions with expansion rules. Theoretical Computer Science, 243, 199–215.CrossRefGoogle Scholar
  24. 24.
    Seldin, J. P. (2000). On lists and other abstract data types in the calculus of constructions. Mathematical Structures in Computer Science, 10, 261–276. Special issue in honor of J. Lambek.CrossRefGoogle Scholar
  25. 25.
    Seldin, J. P. (2001). Extensional set equality in the calculus of constructions. Journal of Logic and Computation, 11(3), 483–493. Presented at festival workshop in foundations and computations held at Heriot-Watt University, Edinburgh, July 16–18, 2000.CrossRefGoogle Scholar
  26. 26.
    Werner, B. (1994). Une théorie des constructions inductives. Ph.D. thesis, Université Paris 7.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2014

Authors and Affiliations

  1. 1.Department of Mathematics and Computer ScienceUniversity of LethbridgeLethbridgeCanada

Personalised recommendations