Abstract
Typing is a way of describing the interactive behavior of algorithms. Usual typing systems are mainly concerned with input-output specifications, e.g., given terms f: A ⇒ B and a: A, the computation of f (a) by normalization yields a result of type B. However, one can dream of more refined typings that would not only ensure ethereal termination, but would for instance yield feasible resource bounds. It seems that time complexity does not lend itself naturally to modular manipulation. We seek something more primitive.
We would like to thank S. Buss, Y. Gurevich, P. Kanellakis, J. Mitchell, A. Nerode, and J. Remel for lively conversations on thos work and also A. Nerode for his help with the literature. This work was begun during a visit by the first and third authors to the Department of Mathematics of the University of Pennsylvania in the fall semester, 1987. They would both like to express their thanks to the department for its hospitality.
Research supported by ONR contract N00014-88K0635, NSF Grant CCR-87-05596, and a Young Faculty Award of the Natural Sciences Association of the University of Pennsylvania.
Research supported by an operating grant from the Natural Sciences and Engineering Research Council of Canada.
On Sabbatical: Dept. of Computer Sciences Stanford University Stanford, CA 94305-2140 U.S.A Arpanet: andre@cs.stanford.edu
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Crossley and A. Nerode. Combinatorial Functors. Springer-Verlag, 1974.
P.J. Freyd and A. Scedrov. Some Semantic Aspects of Polymorphic Lambda Calculus, Second IEEE Symposium on Logic in Computer Science, Ithaca, NY, June, 1987, pp. 315–319.
J-Y. Girard. Linear Logic, Theoretical Computer Science 50, 1987.
J-Y. Girard. Quantifiers in linear logic, in: Proceedings of the SILFS conference Cesena, Italy, January, 1987.
J-Y. Girard. Π 21 03A0 Logic, part 1: dilators, Ann. Math. Logic 21 (1981), pp. 75–219.
J-Y. Girard. Towards a Geometry of Interaction, in: Categories in Computer Science and Logic, ed. by J.W. Gray and A. Scedrov, Contemp. Math, 92, AMS, 1989.
J-Y.Girard. Geometry of Interaction I: Interpretation of system F, in: Logic Colloquium’88, ed. R. Ferro, et al. North-Holland, 1989.
J-Y. Girard, Y.Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.
A. Nerode, J. B. Remmel, and A. Scedrov. Polynomially Graded Logic I: A Graded Version of System T, in: Fourth IEEE Symposium on Logic in Computer Science, Pacific Grove, CA, June, 1989, pp. 375 – 385.
A. Nerode and J. B Remmel. Complexity Theoretic Algebra II: Boolean Algebras, Proc. Third Asian Logic Symp., Ann. Pure & Applied Logic 44 (1989), pp. 71–99.
H.E. Rose. Subrecursion. Oxford Logic Guides 9, 1984.
G.J.Tourlakis. Computability. Reston (Prentice-Hall), 1984.
K.Wagner and G. Wechsung. Computational Complexity. D. Reidel, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Birkhäuser Boston
About this chapter
Cite this chapter
Girard, JY., Scedrov, A., Scott, P.J. (1990). Bounded Linear Logic: A Modular Approach to Polynomial Time Computability. In: Buss, S.R., Scott, P.J. (eds) Feasible Mathematics. Progress in Computer Science and Applied Logic, vol 9. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-3466-1_11
Download citation
DOI: https://doi.org/10.1007/978-1-4612-3466-1_11
Publisher Name: Birkhäuser Boston
Print ISBN: 978-0-8176-3483-4
Online ISBN: 978-1-4612-3466-1
eBook Packages: Springer Book Archive