Logic Journal of IGPL Advance Access originally published online on July 4, 2009
Logic Journal of IGPL 2009 17(5):499-530; doi:10.1093/jigpal/jzp019
This article appears in the following Logic Journal of the IGPL issue: Special Issue: Logical and Semantical Frameworks with Applications [View the issue table of contents]
From light logics to type assignments: a case study
Dipartimento di Informatica, Università degli Studi di Torino. Corso Svizzera 185, 10149 Torino, Italy. E-mail: gaboardi{at}di.unito.it
Dipartimento di Informatica, Universitàa degli Studi di Torino. Corso Svizzera 185, 10149 Torino, Italy. E-mail: ronchi{at}di.unito.it
Using Soft Linear Logic (SLL) as case study, we analyze a method for transforming a light logic into a type assignment system for the 
-calculus, inheriting the complexity properties of the logics. Namely the typing assures the strong normalization in a number of steps polynomial in the size of the term, and moreover all polynomial functions can be computed by -terms that can be typed in the system. The proposed method is general enough to be used also for other light logics.
Key Words: type assignment • implicit computational complexity • lambda calculus • polynomial time
Received for publication 11 May 2008.
References
-
[1] Asperti Andrea. Light affine logic. In: Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS’98), pages 300–308 (1998) IEEE Computer Society.
[2] Asperti Andrea, Roversi Luca. Intuitionistic light affine logic. ACM Transactions on Computational Logic (2002) 3(1):137–175.[CrossRef]
[3] Patrick Baillot, Virgile Mogbil. Soft lambda-calculus: a language for polynomial time computation. In Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’04), volume 2987 of. In: Lecture Notes in Computer Science (2004) Springer.
[4] Patrick Baillot, Terui Kazushige. Light types for polynomial time computation in lambda-calculus. In: Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS’04), pages 266–275 (2004) IEEE Computer Society.
[5] Patrick Baillot, Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation (2009) 207(1):41–62.[CrossRef][Web of Science]
[6] Henk P Barendregt. The lambda; Calculus: Its Syntax and Semantics. (1984) revised. Amsterdam, London, New York: Elsevier/North-Holland.
[7] Coppola Paolo, Dal Lago Ugo, Rocca Simona Ronchi Della. Elementary affine logic and the call by value calculus. In: Proceedings of the 8th International Conference on Typed Lambda-Calculi and Applications (TLCA’05), volume 3461 of Lecture Notes in Computer Science, pages 131–145 (2005) Springer.
[8] Vincent Danos, Jean-Baptiste Joinet. Linear logic and elementary time. Information and Computation (2003) 183(1):123–137.[CrossRef][Web of Science]
[9] Gaboardi Marco. Linearity: an Analytic Tool in the study of Complexity and Semantics of Programming Languages (2007) Università degli Studi di Torino – Institut National Polytechnique de Lorraine. PhD thesis.
[10] Gaboardi Marco, Marion Jean-Yves, Rocca Simona Ronchi Della. A logical account of PSPACE. In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2008, San Francisco, January 10-12, 2008, Proceedings, pages 121–131 (2008).
[11] Gaboardi Marco, Marion Jean-Yves, Rocca Simona Ronchi Della. Soft linear logic and polynomial complexity classes. In: Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2007), volume 205 of Electronic Notes in Theoretical Computer Science, pages 67–87 (2008) Elsevier.
[12] Marco Gaboardi, Simona Ronchi Della Rocca. A soft type assignment system for -calculus. In Proceedings of the 21st International Workshop on Computer Science Logic (CSL’07), volume 4646 of. In: Lecture Notes in Computer Science (2007) Springer. pages 253–267.
[13] Gaboardi Marco, Rocca Simona Ronchi Della. Type inference for a polynomial -calculus. In: Types for proofs and programs 2008, TYPES’08 (2009) Lecture Notes in Computer Science. Springer. Accepted.
[14] Jean-Yves Girard. Linear logic. Theoretical Computer Science (1987) 50:1–102.[CrossRef][Web of Science]
[15] Girard Jean-Yves. Light linear logic. Information and Computation (1998) 143(2):175–204.[CrossRef][Web of Science]
[16] Jean Goubault-Larrecq, Ian Mackie. Proof Theory and Automated Deduction, volume 6 of. In: Applied Logic Series (1997) Dordrecht: Kluwer Academic Publishers.
[17] Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science (2004) 318(1-2):163–180.[CrossRef][Web of Science]
[18] Harry G Mairson, Kazushige Terui. On the computational complexity of cutelimination in linear logic. In ICTCS, volume 2841 of. In: Lecture Notes in Computer Science (2003) Springer.
[19] Simona Ronchi Della Rocca, Luca Roversi. Lambda calculus and intuitionistic linear logic. Studia Logica (1997) 59(3).
[20] Morten H Sørensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of. In: Studies in Logic and the Foundations of Mathematics (2006) Elsevier.
[21] Terui Kazushige. Light affine lambda calculus and polytime strong normalization. In: Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS’01), pages 209–220 (2001) IEEE Computer Society.
[22] Terui Kazushige. Light logic and polynomial time computation (2002) Keio University. PhD thesis.
[23] Wells JB. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic (1999) 98(1–3):111–156.[CrossRef][Web of Science]
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||