Abstract
Light Affine Logic (LAL) is a logical system due to Girard and Asperti offering a polynomial time cut-elimination procedure. It can be used as a type system for lambda-calculus, ensuring a well-typed program has a polynomial time bound on any input. Types use modalities meant to control duplication.
We consider parameterized types where parameters are on the number of modalities and the type instantiation problem: given a term and a parameterized type, does there exist a valuation of the parameters such that the term admits the corresponding type? We show that this type instantiation problem is decidable for normal terms.
This work was partly done while the author was at Laboratoire d’Informatique de Marseille, Universit Aix-Marseille II, Marseille
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Asperti, A. (1998). Light affine logic. In Proceedings LICS’98. IEEE Computer Society Press.
Baillot, P. (2000). Stratified coherent spaces: a denotational semantics for light linear logic. LFCS Tech. report 0025, Univ. of Edinburgh. presented at ICC’00.
Baillot, P. (2001). Checking polynomial time complexity with types (extended version). Tech. report 2001–09, Laboratoire d’Informatique de Paris-Nord.
Bellantoni, S., Niggl, K.-H., and Schwichtenberg, H. (2000). Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic, 104 (1–3).
Coppola, P. and Martini, S. (2001). Typing lambda-terms in elementary logic with linear constraints. In Proceedings TLCA’01,volume 2044 of LNCS. Springer-Verlag.
Danos, V. and Joinet, J.-B. (1999). Linear logic and elementary time. First Workshop on Implicit Computational Complexity (ICC’99).
Danos, V., Joinet, J.-B., and Schellinx, H. (1994). On the linear decoration of intuitionistic derivations. Archive for Mathematical Logic, 33 (6).
Girard, J.-Y. (1998). Light linear logic. Information and Computation, 143: 175–204.
Hofmann, M. (2000). Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic, 104 (1–3).
Leivant, D. and Marion, J.-Y. (1993). Lambda-calculus characterisations of polytime. Fundamenta Informaticae, 19: 167–184.
Roversi, L. (1999). A P-time completeness proof for light logics. In Proceedings CSL’99,volume 1683 of LNCS. Springer-Verlag.
Roversi, L. (2000). Light affine logic as a programming language: a first contribution. International Journal of Foundations of Computer Science, 11 (1).
Schellinx, H. (1994). The Noble Art of Linear Decorating. ILLC Dissertation Series 1994–1, Institute for Language, Logic and Computation, University of Amsterdam.
Terui, K. (2001). Light Affine Lambda-calculus and polytime strong normalization. In Proceedings LICS’01. IEEE Computer Society Press.
Wadler, P. (1991). Is there a use for linear logic? In ACM Conference on Partial Evaluation and Semantics-Based Program Manipulation,New Haven, Connecticut.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media New York
About this chapter
Cite this chapter
Baillot, P. (2002). Checking Polynomial Time Complexity with Types. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds) Foundations of Information Technology in the Era of Network and Mobile Computing. IFIP — The International Federation for Information Processing, vol 96. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35608-2_31
Download citation
DOI: https://doi.org/10.1007/978-0-387-35608-2_31
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5275-5
Online ISBN: 978-0-387-35608-2
eBook Packages: Springer Book Archive