Skip to main content
SpringerLink
Log in

An equational presentation of higher order logic

  • Conference paper
  • First Online:
Book cover Category Theory and Computer Science

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 283))

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Berry, G. “Stable models of the typed λ-calculi” ICALP, Springer-Verlag, LNCS 62, 1978 pp. 72–89

    Google Scholar 

  2. V. Breazu-Tannen and A. Meyer. “Lambda Calculus with Constrained Types” Abstract (1985)

    Google Scholar 

  3. A. Burroni. “Algèbres graphiques” Cahiers de Topologie et Geometrie Differentielle Volume XXII-3 1981

    Google Scholar 

  4. G. Cousineau, P.L. Curien and M. Mauny. “The Categorical Abstract Machine.” In Functional Programming Languages and Computer Architecture, Ed. J. P. Jouannaud, Springer-Verlag LNCS 201 (1985) 50–64.

    Google Scholar 

  5. T. Coquand, C. Gunter, G. Winskel. “Polymorphism and domain equations” Technical report Cambridge no 107.

    Google Scholar 

  6. P. L. Curien. “Categorical Combinators, Sequential Algorithms and Functional Programming.” Research Notes in Theoretical computer Science, Pitman (1986).

    Google Scholar 

  7. P. L. Curien “Categorical combinators for (existential) quantification” unpublished notes.

    Google Scholar 

  8. N.G. de Bruijn. “Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.” Indag. Math. 34,5 (1972), 381–392.

    Google Scholar 

  9. A. Church. “A formulation of the simple theory of types.” Journal of Symbolic Logic 5,1 (1940) 56–68.

    Google Scholar 

  10. P. Gabriel and F. Ulmer. “Lokal Präsentierbare Kategorien” Lecture Notes in Mathematics, Vol. 221 (Springer, Berlin).

    Google Scholar 

  11. R.O. Gandy. “On the axiom of extensionality-Part I.” J.S.L. 21 (1956).

    Google Scholar 

  12. J.Y. Girard. “Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieure.” Thèse d'Etat, Université Paris VII (1972).

    Google Scholar 

  13. J.Y. Girard. “The system F of variable types, fifteen years later” in TCS 86.

    Google Scholar 

  14. C. Gunter. “Profinite Solutions for Recursive Domain Equations” PhD thesis, CMU, (1985).

    Google Scholar 

  15. W. A. Howard. “The formulæ-as-types notion of construction.” Unpublished manuscript (1969). Reprinted in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds J. P. Seldin and J. R. Hindley, Academic Press (1980).

    Google Scholar 

  16. G. Huet. “Cartesian closed categories and Lambda-Calculus” in Combinators and functional programming languages Eds P.L. Curien, G. Cousineau et B. Robinet. LNCS 242

    Google Scholar 

  17. J.M.E. Hyland, P.T. Johnstone, A.M. Pitts. “Tripos theory.” Math. Proc. Camb. Phil. Soc. 88 (1980).

    Google Scholar 

  18. J. Lambek and P. J. Scott. “Introduction to higher order categorical logic” Cambridge studies in advanced mathematics, Cambridge University Press, 1986.

    Google Scholar 

  19. Lawvere. “Adjointness in foundations” Dialectica 23 (1969) 281–296.

    Google Scholar 

  20. P. Martin-Löf. “Intuitionistic Type Theory.” Bibliopolis (1982).

    Google Scholar 

  21. N. McCracken. “An investigation of a programming language with a polymorphic type structure.” Ph.D. Dissertation, Syracuse University (1979).

    Google Scholar 

  22. R. Paré, D. Schumacher. “Indexed Categories and Their Applications.” Springer-Verlag, Lecture Notes in Mathematics, 661.

    Google Scholar 

  23. M.B. Plotkin and G.D. Smyth. “The category-theoretic solution of recursive domain equations” SIAM J. COMPUT. Vol. 11, No 4, November 1982

    Google Scholar 

  24. D. Scott. “Relating Theories of the Lambda-Calculus.” in To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Eds. J. P. Seldin and J. R. Hindley, Academic Press (1980).

    Google Scholar 

  25. R.A.G. Seely. “Hyperdoctrines, natural deduction and the Beck condition” Zeitschrift für Mat. Logik und Grundlagen d. Math. 29 505–542.

    Google Scholar 

  26. R.A.G Seely. “Locally Cartesian Closed Categories and Type Theory” Math. Proc. Camb. Phil. Soc. 95, 1984.

    Google Scholar 

  27. R.A.G. Seely. “Categorical Semantics for Higher Order Polymorphic Lambda Calculus” Draft.

    Google Scholar 

  28. J.E. Stoy. “Denotational Semantics: the Scott-Strache Approach to the Programming Language Theory” The M.I.T. Press, Cambridge, Massachussetts, and London, England.

    Google Scholar 

  29. G. Takeuti. “Proof theory.” Studies in Logic 81 Amsterdam (1975).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, ENS and Cambridge

    Thierry Coquand & Thomas Ehrhard

Authors
  1. Thierry Coquand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Ehrhard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

David H. Pitt Axel Poigné David E. Rydeheard

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coquand, T., Ehrhard, T. (1987). An equational presentation of higher order logic. In: Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds) Category Theory and Computer Science. Lecture Notes in Computer Science, vol 283. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18508-9_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-18508-9_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-18508-6

  • Online ISBN: 978-3-540-48006-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation