A Polymorphic Language Which Is Typable and Poly-step

  • Luca Roversi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1538)


A functional language ΛLA is given. A sub-set ΛLA T of ΛLA is automatically typable. The types are formulas of Intuitionistic Light Affine Logic with polymorphism à la ML. Every term of ΛLA T can reduce to its normal form in, at most, poly-steps. ΛLA T can be used as a prototype of programming language for P-TIME algorithms


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Asperti. Light Affine Logic. In Proceedings of Symposium on Logic in Computer Science LICS’98, 1998.Google Scholar
  2. [2]
    L. Damas and R. Milner. Principal type-schemes for functional programs. In Proceedings of Symposium on Logic in Computer Science LICS’82, January 1982.Google Scholar
  3. [3]
    J.-Y. Girard. Light Linear Logic. Information and Computation, 143:175–204, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.Google Scholar
  5. [5]
    C.A. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. The MIT Press, 1992.Google Scholar
  6. [6]
    M. Hoffmann. A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. In Proceedings of Computer Science Logic 1997 (CSL’97), Aarhus, Denmark, volume To appear, 1997.Google Scholar
  7. [7]
    D. Leivant and J.-Y. Marion. Lambda calculus characterizations of poly-time. Fundamenta Informaticae, 19:167–184, 1993.zbMATHMathSciNetGoogle Scholar
  8. [8]
    R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.Google Scholar
  9. [9]
    G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.zbMATHCrossRefMathSciNetGoogle Scholar
  10. [10]
    L. Roversi. Concrete syntax for intuitionistic light affine logic with polymorphic type assignment. In Theoretical Computer Science: Proceedings of the Sixth Italian Conference (Prato). World Scientific (TO APPEAR), 9–11 November 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Luca Roversi
    • 1
  1. 1.Institute de Mathématiques de LuminyMarseille Cedex 9France

Personalised recommendations