zbMATH — the first resource for mathematics

Computational interpretations of linear logic. (English) Zbl 0791.03003
Author’s abstract: We study Girard’s linear logic from the point of view of giving a concrete computational interpretation of the logic, based on the Curry-Howard isomorphism. In the case of intuitionistic linear logic, this leads to a refinement of the lambda calculus, giving finer control over order of evaluation and storage allocation, while maintaining the logical content of programs as proofs, and computation as cut- elimination. In the classical case, it leads to a concurrent process paradigm with an operational semantics in the style of Berry and Boudol’s chemical abstract machine. This opens up a promising new approach to parallel implementation of functional programming languages; and offers the prospect of typed concurrent programming in which correctness is guaranteed by the typing.

03B20 Subsystems of classical logic (including intuitionistic logic)
68Q55 Semantics in the theory of computing
03B70 Logic in computer science
03B40 Combinatory logic and lambda calculus
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03F05 Cut-elimination and normal-form theorems
Full Text: DOI
[1] Abramsky, S., Computational interpretations of linear logic, () · Zbl 0791.03003
[2] ()
[3] Barendregt, H., ()
[4] H. Barendregt and K. Hemerik, Types in lambda calculi and programming languages, in: Proc. ESOP ’90. · Zbl 0770.03005
[5] Berry, G.; Boudol, G., The chemical abstract machine, Conf. record of the 17th ann. ACM symp. on principles of programming languages, 81-94, (1990)
[6] Bird, R.; Wadler, P., Introduction to functional programming, (1988), Prentice-Hall Englewood Cliffs, NJ
[7] Cohn, P.M., Universal algebra, (1981), Reidel Dordrecht · Zbl 0141.01002
[8] Damas, L.; Milner, R., Principal type schemes for functional programs, Conf. record of the 9th ann. ACM symp. on the principles of programming languages, 207-212, (1982)
[9] Field, A.J.; Harrison, P.G., Functional programming, (1988), Addison-Wesley Reading, MA · Zbl 0828.68033
[10] Gallier, J., On Girard’s “candidats de reductibilité”, ()
[11] Girard, J.-Y., Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur, (1972), Ph.D. Thesis, University of Paris VII
[12] Girard, J.-Y., Linear logic, Theoret. comput. sci., 50, 1-102, (1987) · Zbl 0625.03037
[13] Girard, J.-Y., Geometry of interaction 1: interpretation of system F, ()
[14] Girard, J.-Y., Towards a geometry of interaction, (), 69-108, Contemporary Mathematics
[15] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, Vol. 7, (1989), Cambridge University Press Cambridge, Cambridge Tracts in Theoretical Computer Science
[16] Girard, J.-Y.; Scedrov, A.; Scott, P.J., Bounded linear logic, ()
[17] (), Lecture Notes in Computer Science
[18] Henderson, P., Functional programming: applications and implementation, (1980), Prentice-Hall Englewood Cliffs, NJ
[19] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[20] Holmström, S., Linear functional programming, (), 13-32
[21] Hudak, P.; Wadler, P., Report on the functional programming language Haskell, ()
[22] ()
[23] Karlsson, K., ()
[24] Kahn, G., Natural semantics, (), 22-39, Lecture Notes in Computer Science · Zbl 0657.68079
[25] Lafont, Y., The linear abstract machine, Theoret. comput. sci., 59, 157-180, (1988) · Zbl 0648.68016
[26] Landin, P.J., The mechanical evaluation of expressions, Comput. J., 6, 308-320, (1964) · Zbl 0122.36106
[27] Landin, P.J.; Landin, P.J., A correspondence between ALGOL 60 and Church’s lambda notation, Comm. ACM, Comm. ACM, 8, 158-165, (1965) · Zbl 0134.33403
[28] INMOS LTD, Occam 2 reference manual, (1988), Prentice-Hall Englewood Cliffs, NJ
[29] Martin-Löf, P., Intuitionistic type theory, Vol. 443, (1984), Bibliopolis Naples
[30] McCarthy, J., A basis for a mathematical theory of computation, (), 33-69
[31] Meyer, A.; Cosmodakis, S., Semantical paradigms, (), 236-255
[32] Milner, R., A calculus for communicating systems, Vol. 92, (1980), Springer Berlin, Lecture Notes in Computer Science · Zbl 0452.68027
[33] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[34] Milner, R., Functions as processes, (), 167-180, Lecture Notes in Computer Science · Zbl 0766.68036
[35] Milner, R.; Tofte, M.; Harper, R., The definitions of standard ML, (1990), MIT Press Cambridge, MA
[36] Mitchell, J.C.; Plotkin, G.D., Abstract types have existential type, Conf. record of the 12th ann. ACM symp. on principles of programming languages, 37-51, (1985)
[37] Mycroft, A., The theory of practice of transforming call-by-need into call-by-value, (), Lecture Notes in Computer Science · Zbl 0435.68015
[38] Peyton Jones, S.L., The implementation of functional programming languages, (1987), Prentice-Hall Englewood Cliffs, NJ · Zbl 0712.68017
[39] Plotkin, G.D., Call-by-name, call-by-value and the lambda calculus, Comput. sci., 1, 125-159, (1975) · Zbl 0325.68006
[40] Plotkin, G.D., Lectures on predomains and partial functions, Notes for a course given at the center for the study of language and information, Stanford, (1985)
[41] Reynolds, J.C., Three approaches to type structure, (), 97-138, Lecture Notes in Computer Science
[42] Sands, D., Complexity analysis for a lazy higher order language, Proc. 2nd Glasgow workshop on functional programming, (1989)
[43] Solitro, U., A typed calculus based on a fragment of linear logic, Theoret. comput. sci., 68, 333-342, (1989) · Zbl 0694.03035
[44] Turner, D.A., Miranda - a non-strict functional language with polymorphic types, (), Lecture Notes in Computer Science · Zbl 0592.68014
[45] ()
[46] Valentini, S., The judgement calculus for intuitionistic linear logic: proof theory and semantics, () · Zbl 0739.03008
[47] Wadler, P., Linear types can change the world!, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.