Skip to main content
SpringerLink
Log in

Highlighting the lambda-free fragment of Automath

  • Invited Paper
  • Conference paper
  • First Online:
Higher Order Logic Theorem Proving and Its Applications (HUG 1994)

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

Included in the following conference series:

  • 119 Accesses

Abstract

Pal is the fragmant of Automath that does not use lambda calculus. It just deals with typed definitions in typed contexts. Its powers and weaknesses are discussed here.

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. Selected Papers on Automath, edited by R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer, Studies in Logic, North-Holland Publishing Co., to appear 1994.

    Google Scholar 

  2. N.G. de Bruijn: Automath, a language for mathematics. Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05, 47 p., 1968. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag 1983, pp. 159–200.

    Google Scholar 

  3. -: The mathematical language Automath, its usage, and some of its extensions. Symposium on Automatic Demonstration (Versailles December 1968), Lecture Notes in Mathematics vol. 125, Springer Verlag 1970, pp. 29–61. To be reprinted in [1].

    Google Scholar 

  4. -: Automath, a language for mathematics. Séminaire Math. Sup. 1971. Les Presses de l'Université de Montréal 1973, 58 p.

    Google Scholar 

  5. -: AUT-SL, a single line version of Automath. Report, Department of Mathematics, Eindhoven University of Technology, 1971. To be reprinted in [1].

    Google Scholar 

  6. -: A survey of the project Automath. In: To H.B. Curry: Essays in combinatory logic, lambda calculus and formalism, ed. J.P. Seldin and J.R. Hindley, Academic Press 1980, pp. 579–606.

    Google Scholar 

  7. -: Formalization of constructivity in Automath. In: Papers dedicated to J.J. Seidel, ed. P.J. de Doelder, J. de Graaf and J.H. van Lint. EUT-Report 84-WSK-03, ISSN 0167-9708, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1984, pp. 76–101. To be reprinted in [1].

    Google Scholar 

  8. -: Generalizing Automath by means of a lambda-typed lambda calculus. In: Mathematical Logic and Theoretical Computer Science, Lecture Notes in pure and applied mathematics, 106, (ed. D. W. Kueker, E.G.K. Lopez-Escobar, C.H. Smith) pp. 71–92. Marcel Dekker, New York 1987.

    Google Scholar 

  9. -: The use of justification systems for integrated semantics In: Colog-88, International Conference on Computer Logic Tallinn USSR, December 1988, Proceedings. Ed. P. artin-Löf and G. Mints. Lecture Notes in Computer Science Nr. 417, pp. 9–24. Springer-Verlag 1990.

    Google Scholar 

  10. -: Checking mathematics with computer assistance. Notices American Mathematical Society, vol 8(1), Jan. 1991, pp 8–15.

    Google Scholar 

  11. -: Algorithmic definition of lambda-typed lambda calculus. In: Logical Environments. Editors G. Huet and G. Plotkin. Cambridge University Press 1993, pp. 131–146.

    Google Scholar 

  12. -: Reflections on Automath. In: Selected Papers on Automath, edited by R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer, Studies in Logic, North-Holland Publishing Co., to appear 1994.

    Google Scholar 

  13. -: On the roles of types in mathematics. To be published.

    Google Scholar 

  14. D.T. van Daalen: The language theory of Automath. Ph.D. thesis, Eindhoven University of Technology, 1980. Parts of this thesis will be reprinted in [1].

    Google Scholar 

  15. R.P. Nederpelt. Strong normalization in a typed lambda calculus with lambda structured types. Ph.D. thesis, Eindhoven University of Technology, 1973. Parts of this thesis will be reprinted in [1].

    Google Scholar 

  16. L.S. van Benthem Jutting: Checking Landau's “Grundlagen” in the Automath system. Ph.D. Thesis, Eindhoven University of Technology, 1977. Mathematical Centre Tracts nr. 83, Amsterdam 1979. Parts of this thesis will be reprinted in [1].

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, Eindhoven, The Netherlands

    N. G. de Bruijn

Authors
  1. N. G. de Bruijn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Thomas F. Melham Juanito Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Bruijn, N.G. (1994). Highlighting the lambda-free fragment of Automath. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_36

Download citation

  • DOI: https://doi.org/10.1007/3-540-58450-1_36

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48803-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation