Proofs as Efficient Programs

  • Ugo Dal Lago
  • Simone Martini


Logic and theory of computation have been intertwined since their first days. The formalized notion(s) of effective computation are at first technical tools for the investigation of first order systems, and only ten years later — in the hands of John von Neumann — become the blueprints of engineered physical devices. Generally, however, one tends to forget that in those same years, in the newly-born proof-theory of Gerhard Gentzen [20] there is an implicit, powerful notion of computation-an effective, combinatorial procedure for the simplification of a proof. However, the complexity of the rules for the elimination of cuts (especially the commutative ones, in the modern jargon) hid the simplicity and generality of the basic computational notion those rules were based upon. We had to wait thirty more years before realizing in full glory that Gentzen's simplification mechanism and one of the formal systems for computability (Church's λ-calculus) were indeed one and the same notion.


Normal Form Turing Machine Cost Model Complexity Class Linear Logic 
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.
    A. Asperti and S. Guerrini: The Optimal Implementation of Functional Programming Languages (Cambridge University Press, Cambridge 1998)Google Scholar
  2. 2.
    A. Asperti and L. Roversi: Intuitionistic Light Affine Logic. ACM Transactions on Computational Logic 3, 1 (2002) pp 137–175CrossRefGoogle Scholar
  3. 3.
    P. Baillot: Approches dynamiques en semantique de la logique lineaire: jeux et gèometrie de l’interaction. (Universite Aix-Marseille 2, 1999)Google Scholar
  4. 4.
    P. Baillot: Stratified coherence spaces: a denotational semantics for light linear logic. TCS 318, 1-2 (2004) pp 29–55CrossRefGoogle Scholar
  5. 5.
    P. Baillot, P. Coppola and U. Dal Lago: Light Logics and Optimal Reduction: Completeness and Complexity. In: 22nd LICS (IEEE Comp. Soc., 2007) pp 421–430Google Scholar
  6. 6.
    P. Baillot and M. Pedicini: Elementary Complexity and Geometry of Interaction. Fundamenta Informaticae 45, 1-2 (2001) pp 1–31Google Scholar
  7. 7.
    P. Baillot and K. Terui: Light Types for Polynomial Time Computation in Lambda-Calculus. In: LICS 2004 (IEEE Comp. Soc., 2004) pp 266–275Google Scholar
  8. 8.
    A. Church: A set of postulates for the foundation of logic. Ann. of Math. (2) 33 (1932) pp 346–366CrossRefGoogle Scholar
  9. 9.
    S. Cook and A. Urquhart: Functional Interpretations of Feasible Constructive Arithmetic. Annals of Pure and Applied Logic 63, 2 (1993) pp 103–200CrossRefGoogle Scholar
  10. 10.
    J. Crossley, G. Mathai and R. Seely: A Logical Calculus for Polynomial-time Realizability. Journal of Methods of Logic in Computer Science, 3 (1994) pp 279–298Google Scholar
  11. 11.
    H. B. Curry and R. Feys: Combinatory Logic, vol. 1 (North-Holland, Amsterdam 1958)Google Scholar
  12. 12.
    N. Cutland: Computability: An Introduction to Recursive Function Theory (Cambridge University Press, Cambridge 1980)Google Scholar
  13. 13.
    U. Dal Lago: The Geometry of Linear Higher-Order Recursion. In: 20th LICS (IEEE Comp. Soc., 2005) pp 366–375Google Scholar
  14. 14.
    U. Dal Lago: Context Semantics, Linear Logic and Computational Complexity. In: 21st LICS (IEEE Comp. Soc., 2006) pp 169–178Google Scholar
  15. 15.
    U. Dal Lago and M. Hofmann: Quantitative Models and Implicit Complexity. Proc. Found. of Software Techn. and Theor. Comp. Sci. (2005) pp 189–200Google Scholar
  16. 16.
    U. Dal Lago and S. Martini: An Invariant Cost Model for the Lambda Calculus. In:Logical Approaches to Computational Barriers. LNCS 3988 (Springer-Verlag, Berlin Heidelberg New York 2006)Google Scholar
  17. 17.
    U. Dal Lago and S. Martini: Beta Reduction is a Cost Model for the Weak Lambda Calculus. Available from the authors (2007)Google Scholar
  18. 18.
    V. Danos and L. Regnier: Proof-nets and Hilbert space. In: Advances in Linear Logic, ed by J.-Y. Girard, Y. Lafont and L. Regnier (Cambridge University Press, Cambridge 1995) pp 307–328Google Scholar
  19. 19.
    M. Gaboardi, J.-Y. Marion and S. Ronchi Della Rocca: Proceedings of 35th ACM POPL. A Logical Account of PSPACE. To appearGoogle Scholar
  20. 20.
    G. Gentzen: Untersuchungen öber das logische Schließen I and II. Mathematische Zeitschrift 39, 1 (1935) pp 176–210; 405-431CrossRefGoogle Scholar
  21. 21.
    J.-Y. Girard: Proof Theory and Logical Complexity, I (Bibliopolis, Napoli 1987)Google Scholar
  22. 22.
    J.-Y. Girard: Linear Logic. TCS 50 (1987) pp 1–102CrossRefGoogle Scholar
  23. 23.
    J.-Y. Girard: Geometry of interaction 2: deadlock-free algorithms. In: COLOG-88: Proc. of the int. conf. on Computer logic. LNCS. 417 (Springer-Verlag, Berlin Heidelberg New York 1988) pp 76–93Google Scholar
  24. 24.
    J.-Y. Girard: Geometry of Interaction 1: Interpretation of system F. In: Proc. Logic Colloquium’ 88 (North-Holland, Amsterdam 1989) pp 221–260Google Scholar
  25. 25.
    J.-Y Girard: Light Linear Logic. Inform. and Comp. 143, 2 (1998) pp 175–204CrossRefGoogle Scholar
  26. 26.
    G. Gonthier, M. Abadi and J.-J. Lévy: The Geometry of Optimal Lambda Reduction. In: Proc. 12th ACM POPL (1992) pp 15–26Google Scholar
  27. 27.
    W. A. Howard: The Formulae-as-Types notion of Construction. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, ed by J. P. Seldin and J. R. Hindley (Academic Press Inc., New York 1980) pp 479–490Google Scholar
  28. 28.
    G. Kreisel: Interpretation of analysis by means of constructive functions of finite types. In: Constructivity in Mathematics, ed by A. Heyting (North-Holland, Amsterdam 1959) pp 101–128Google Scholar
  29. 29.
    Y. Lafont: Soft Linear Logic and Polynomial Time. TCS 318 (2004) pp 163–180CrossRefGoogle Scholar
  30. 30.
    O. Laurent and L. Tortora de Falco: Obsessional Cliques: A Semantic Characterization of Bounded Time Complexity. In: LICS (2006) pp 179–188Google Scholar
  31. 31.
    I. Mackie: The Geometry of Interaction Machine. In: Proc. 22nd ACM POPL (1995) pp 198–208Google Scholar
  32. 32.
    A. S. Murawski and C.-H. L. Ong: Discreet Games, Light Affine Logic and PTIME Computation. CSL (2000) pp 427–441Google Scholar
  33. 33.
    J. S. Pinto: Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction. Proc. 5th International Conference on Typed Lambda Calculi and Applications (2001) pp 385–399Google Scholar
  34. 34. G. D. Plotkin: Call-by-Name, Call-by-Value and the lambda-Calculus. TCS 1, 2 (1975) pp 125–159CrossRefGoogle Scholar
  35. 35.
    D. Sands, J. Gustavsson and A. Moran: Lambda Calculi and Linear Speedups. In: The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. LNCS 2566 (Springer-Verlag, Berlin Heidelberg New York 2002)Google Scholar
  36. 36.
    R. Statman: The Typed lambda-Calculus is not Elementary Recursive. TCS 9 (1979) pp 73–81Google Scholar
  37. 37.
    K. Terui: Light affine lambda calculus and polynomial time strong normalization. Arch. Math. Log. 46, 3-4 (2007) pp 253–280CrossRefGoogle Scholar
  38. 38.
    A. S. Troelstra: Realizability. In: Handbook of Proof Theory, ed by S. Buss (Elsevier, 1998) pp 407–473Google Scholar
  39. 39.
    P. van Emde Boas: Machine Models and Simulation. In: Handbook of Theoretical Computer Science, vol A: Algorithms and Complexity (A), (MIT Press, Boston 1990) pp 1–66Google Scholar
  40. 40. C. P. Wadsworth: Semantics and pragmatics of the lambda-calculus. Phd Thesis, Chapter 4 (1971)Google Scholar

Copyright information

© Springer-Verlag Italia 2008

Authors and Affiliations

  • Ugo Dal Lago
    • 1
  • Simone Martini
    • 1
  1. 1.Dipartimento di Scienze dell’InformazioneUniversità di BolognaBolognaItaly

Personalised recommendations