Controlling Program Extraction in Light Logics

  • Marc Lasson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


We present two refinements, based on program extraction in elementary affine logic and light affine logic, of Krivine & Leivant’s system FA2. This system allows higher-order equations to specify the computational content of extracted programs. The user can then prove a generic formula, using these equations as axioms. The system guarantees that the extracted program satisfies the specification and is computable in elementary time (for elementary affine logic) or polynomial time (for light affine logic). Finally, we show that both systems are complete with respect to elementary time and polynomial time functions.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Asperti, A., Roversi, L.: Intuitionistic Light Affine Logic. ACM Trans. Comput. Log. 3(1), 137–175 (2002)CrossRefGoogle Scholar
  2. 2.
    Baillot, P.: Type inference for light affine logic via constraints on words. Theoretical Computer Science 328, 289–323 (2004)CrossRefzbMATHGoogle Scholar
  3. 3.
    Bernardy, J.-P., Lasson, M.: Realizability and parametricity in pure type systems. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 108–122. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Danos, V., Joinet, J.B.: Linear Logic & Elementary Time. Information and Computation 183 (2001)Google Scholar
  5. 5.
    Girard, J.Y.: Light Linear Logic. Information and Computation 143(2), 175–204 (1998)CrossRefzbMATHGoogle Scholar
  6. 6.
    Krivine, J.L.: Lambda-calculus, types and models. Ellis Horwood, England (1993)zbMATHGoogle Scholar
  7. 7.
    Krivine, J.L., Parigot, M.: Programming with Proofs. Elektronische Informationsverarbeitung und Kybernetik 26(3), 149–167 (1990)zbMATHGoogle Scholar
  8. 8.
    Leivant, D.: Reasoning about Functional Programs and Complexity Classes Associated with Type Disciplines. In: FOCS, pp. 460–469. IEEE, Los Alamitos (1983)Google Scholar
  9. 9.
    Martini, S., Coppola, P.: Typing lambda terms in elementary logic with linear constraints. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 76–90. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Plotkin, G.D., Abadi, M., Cardelli, L.: Subtyping and parametricity. In: LICS, pp. 310–319. IEEE Computer Society, Los Alamitos (1994)Google Scholar
  11. 11.
    Rose, H.: Sub-recursion: functions and hierarchy. Oxford University Press, Oxford (1984)Google Scholar
  12. 12.
    Takeuti, I.: An Axiomatic System of Parametricity. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 354–372. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Wadler, P.: The Girard-Reynolds isomorphism (second edition). Theor. Comput. Sci. 375(1-3), 201–226 (2007)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Marc Lasson
    • 1
  1. 1.ENS Lyon, Université de Lyon, LIPFrance

Personalised recommendations