The Completeness of BCD for an Operational Semantics

  • Rick StatmanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


The theorem of Coppo et al. ([3, 6]) states that an untyped lambda term is strongly normalizable if and only if it provably has an intersection type. Here we consider which terms have which types.


Lambda calculus Intersection types Completeness theorem Operational semantics 


  1. 1.
    Barendregt, H.P.: The Lambda Calculus. North Holland, New York (1981)zbMATHGoogle Scholar
  2. 2.
    Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, New York (2013)CrossRefzbMATHGoogle Scholar
  3. 3.
    Coppo, M., Dezani, M.: A new type assignment for lambda terms. Archiv fur Math. Logik 19, 139–156 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    van Dalen, D.: Intuitionistic logic. In: Gobble, L. (ed.) The Blackwell Guide to Philosophical Logic. Blackwell, Oxford (2001)Google Scholar
  5. 5.
    Plotkin, G.D.: Lambda definability in the full type hierarchy. In: Hindley, J.R., Seldin, J.P. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363–373. Academic Press, London (1980)Google Scholar
  6. 6.
    Pottinger, G.: A type assignment for the strongly normalizable lambda terms. In: Hindley, J., Seldin, J. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577. Academic Press, London (1980)Google Scholar
  7. 7.
    Statman, R.: Logical relations and the typed lambda calculus. Inf. Contr. 165(2/3), 85–97 (1985)CrossRefzbMATHGoogle Scholar
  8. 8.
    Tait, W.W.: Constructive reasoning. In: Van Rootselaar, B., Staal, J.F. (eds.) Studies in Logic and the Foundations of Mathematics, vol. 52, pp. 185–199. Elsevier, NorthHolland (1968)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Department of Mathematical SciencesCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations