Some results on the full abstraction problem for restricted lambda calculi

  • Furio Honsell
  • Marina Lenisa
Invited Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


Issues in the mathematical semantics of two restrictions of the λ-calculus, i.e. λI-calculus and λv-calculus, are discussed. A fully abstract model for the natural evaluation of the former is defined using complete partial orders and strict Scott-continuous functions. A correct, albeit non-fully abstract, model for the SECD evaluation of the latter is denned using Girard's coherence spaces and stable functions. These results are used to illustrate the interest of the analysis of the fine structure of mathematical models of programming languages.


Normal Form Stable Function Operational Semantic Denotational Semantic Coherence Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Barendregt, H.: The Lambda, Calculus, its Syntax and Semantics. North Holland. Amsterdam (1984)Google Scholar
  2. 2.
    Böhm, C.: Lambda Calculus and Computer Science Theory. LNCS 37 Springer-Verlag (1975)Google Scholar
  3. 3.
    Church, A.: The Calculi of Lambda Conversion. Princeton University Press Princeton (1941)Google Scholar
  4. 4.
    Coppo, M., Dezani-Ciancaglini, M., Zacchi, M.: Type Theories, Normal Forms and D -Lambda-Models. Information and Computation 72(2) (1987) 85–116Google Scholar
  5. 5.
    Dezani-Ciancaglini, M., Honsell, F., Ronchi Della Rocca, S.: Models for theories of functions depending on all their arguments (abstract). Journal of Symbolic Logic 51(3) (1986) 399–402Google Scholar
  6. 6.
    Egidi, L., Honsell, F., Ronchi Della Rocca, S.: Operational, Denotational and Logical descriptions: a case study. Fundamenta Informaticae 16(2) (1992) 149–169Google Scholar
  7. 7.
    Girard, J.Y.: The system F of variable types, fifteen years later. TCS 45 (1986) 159–192Google Scholar
  8. 8.
    Girard, J. Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press. Cambridge (1989)Google Scholar
  9. 9.
    Hindley, J. R., Longo, G.: Lambda Calculus Models and Extensionality. Z. Math. Logik Grundlag. Math. 26 (1980) 289–310Google Scholar
  10. 10.
    Landin, P. J.: The mechanical evaluation of expressions. Computer J. 6(4) (1964) 308–320Google Scholar
  11. 11.
    Meyer, A.: What is a, Model of the Lambda Calculus? Information and Control 52 (1982) 87–122Google Scholar
  12. 12.
    Plotkin, G. D.: Call-by-name, call-by-value and the λ-calculus. TCS 1 (1975) 125–159Google Scholar
  13. 13.
    Smith, M. B., Plotkin, G. D.: The category-theoretic solution of recursive domain equations. SIAM J. of Computing 11(5) (1982) 761–783Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Furio Honsell
    • 1
  • Marina Lenisa
    • 1
  1. 1.Dipartimento di Matematica e InformaticaUniversità di UdineItaly

Personalised recommendations