Abstract
The simply typed lambda calculus, of these notes, has types built up from atomic types using the function type operation that forms a new typeA→Bfrom typesA,B.The calculus can be viewed as a refined version of the purely implicational fragment of intuitionistic logic. The refinement consists in using terms of the untyped lambda calculus to represent formal derivations of the logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
H. BarendregtThe Lambda CalculusNorth Holland Publishing Co., Amsterdam. 2nd edition, 1984.
J. Gallier, “On Girard’s ”Candidats de Reductibilité“, inLogic and Computer Scienceed. P. Odifreddi, Vol. 31 in APIC studies in Data Processing, pp. 123–203, Academic Press, 1990.
J. Gallier, “Constructive Logics, Part I: A tutorial on proof systems and typed A-calculi”Theoretical Computer Science 110249–339, 1991.
J. Girard, Y. Lafont and P. TaylorProofs and TypesCambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989.
J. Lambek and P.J. ScottIntroduction to higher order categorical logicCambridge Studies in Advanced Mathematics 7, Cambridge University Press, 1986.
P. Martin-LofIntuitionistic Type TheoryBibliopolis, Napoli, 1984.
B. Nordstrom, K. Petersson and J. SmithProgramming in Martin-Lof’s Type Theory An InroductionMonographs on Computer Science 7, Oxford University Press, 1990.
B. Nordstrom and K. Petersson and J. Smith, “Martin-Lof’s Type Theory.” A chapter inHandbook of Logic in Computer Sciencewritten in 1994, to appear. (Available by ftp fromftp://ftp.cs.chalmers.se)/pub/csreports/papers/smith/hlcs.ps.gz
M. Takahashi, “Parallel Reductions in λ-Calculus”Information and Computation118, 120–127, 1995.
A. S. Troelstra and H. Schwichtenberg, Basic Proof TheoryCambridge Tracts in Theoretical Computer Science 43Cambridge University Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aczel, P. (1999). Notes on the Simply Typed Lambda Calculus. In: Berger, U., Schwichtenberg, H. (eds) Computational Logic. NATO ASI Series, vol 165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-58622-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-58622-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-63670-7
Online ISBN: 978-3-642-58622-4
eBook Packages: Springer Book Archive