Filter models for a parallel and non deterministic λ-calculus

Extended abstract
  • Mariangiola Dezani-Ciancaglini
  • Ugo de'Liguoro
  • Adolfo Piperno
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


The distinction between the conjunctive nature of non-determinism as opposed to the disjunctive character of parallelism constitutes the motivation and the starting point of the present work. λ-calculus is extended with both a non-deterministic choice and a parallel operator; a notion of reduction is introduced, extending β-reduction of the classical calculus.

We study type assignment systems for this calculus, together with a denotational semantics which is initially defined constructing a set semimodel via simple types. We enrich the type system with intersection and union types, dually reflecting the disjunctive and conjunctive behaviour of the operators; we build a filter model whose local structure is compared with a Morris-style operational semantics.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi, “A Semantics for Static Type Inference in a Nondeterministic Language”, to appear in Information and Computation.Google Scholar
  2. 2.
    S. Abramsky, “Domain Theory in Logical Form”, Ann. of Pure and Appl. Logics, 51, 1991, 1–77.Google Scholar
  3. 3.
    E.A. Ashcroft, M.C.B. Hennessy, “A Mathematical Semantics for a Non Deterministic Typed Lambda Calculus”, TCS 11, 1980, 227–245.Google Scholar
  4. 4.
    F. Barbanera, M. Dezani-Ciancaglini, “Intersection and Union Types”, TACS'91, LNCS 526, 1991, 651–674.Google Scholar
  5. 5.
    H.P. Barendregt, The Lambda-Calculus: Its Syntax and Semantics, North-Holland, Amsterdam 1984.Google Scholar
  6. 6.
    H. Barendregt, M. Coppo, M. Dezani-Ciancaglini, “A Filter Lambda Model and the Completeness of Type Assignment”, J.Symbolic Logic 48, 1983, 931–940.Google Scholar
  7. 7.
    G. Boudol, “A Lambda Calculus for (Strict) Parallel Functions”, INRIA-Sophia Antipolis Tech. Rep. 1387, 1991, to appear in Information and Computation.Google Scholar
  8. 8.
    M. Dezani-Ciancaglini, U. de'Liguoro, A. Piperno, “Filter Models for a Parallel and Non Deterministic λ-calculus”, Internal report, Un. di Roma I, 1993.Google Scholar
  9. 9.
    R. Hindley, “The Completeness Theorem for Typing λ-terms”, TCS 22, 1983, 1–17.Google Scholar
  10. 10.
    R. Hindley, G. Longo, “Lambda Calculus Models and Extensionality”, Z. Math. Logik 26, 1980, 289–310.Google Scholar
  11. 11.
    J.L. Krivine, Lambda-calcul, types et modèles, Masson, Paris 1990.Google Scholar
  12. 12.
    U. de' Liguoro, “Non-deterministic Untyped λ-calculus”, PhD Thesis, Un. di Roma I, 1991.Google Scholar
  13. 13.
    U. de' Liguoro, A. Piperno, “Must Preorder in Non-deterministic Untyped λ-calculus”, CAAP '92, LNCS 582, 1992, 203–220.Google Scholar
  14. 14.
    J.H. Morris, Lambda Calculus Models of Programming Languages, Dissertation, M.I.T. 1968.Google Scholar
  15. 15.
    C.-H.L. Ong, “Concurrent Lambda Calculus and a General Precongruence Theorem for Applicative Bisimulations”, Draft, Cambridge Un., 1992.Google Scholar
  16. 16.
    C.-H.L. Ong, “Non-Determinism in a Functional Setting”, to appear in LICS '93.Google Scholar
  17. 17.
    G.D. Plotkin, “LCF considered as a programming language”, TCS, 5, 1977, 223–256.Google Scholar
  18. 18.
    G.D. Plotkin, “A Powerdomain Construction”, SIAM J. of Comp. 3, 1976, 452–487.Google Scholar
  19. 19.
    G. D. Plotkin, “A Semantics for Static Type Inference”, to appear in Information and Computation. A preliminary version in TACS'91, LNCS 526, 1991, 1–17.Google Scholar
  20. 20.
    D. Sangiorgi, “The Lazy λ-calculus in a Concurrency Scenario”, LICS'92, 1992, 102–109.Google Scholar
  21. 21.
    M.B. Smith, “A Power Domains”, J. Comp. Sys. Sci. 16, 1978, 23–36.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Mariangiola Dezani-Ciancaglini
    • 1
  • Ugo de'Liguoro
    • 1
  • Adolfo Piperno
    • 2
  1. 1.Dipartimento di InformaticaUniversitá di TorinoTorinoItaly
  2. 2.Dipartimento di Scienze dell'InformazioneUniversità di Roma “La Sapienza”RomaItaly

Personalised recommendations