Axioms and models of linear logic. (English) Zbl 0703.03010

This paper presents J.-Y. Girard’s recent system of linear logic [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] in a manner so as to avoid the two-level structure of formulae and sequents. A Hilbert- style formulation of linear logic is presented with a deduction theorem, which is proved to be equivalent to Girard’s sequent calculus. Various models are investigated. Some related and partly overlapping work can be found in work of A. Avron [Theor. Comput. Sci. 57, No.2/3, 161-184 (1988; Zbl 0652.03018)].
Reviewer: H.Nishimura


03B70 Logic in computer science
03F99 Proof theory and constructive mathematics
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI


[1] Avron, A.: The Semantics and Proof Theory of Linear Logic. ECS-LFCS-87-27, Edinburgh, 1987.
[2] Dijkstra, E. W. and Scholten, C. S.:Predicate Calculus and Program Semantics, Springer Verlag, 1990. · Zbl 0698.68011
[3] Dunn, J. M.: Relevance Logic and Entailment. In:Handbook of Philosophical Logic, D. Gabbay and F. Günther (eds) Vol. III, pp. 117–224 Reidel Publ. Cie 1986. · Zbl 0875.03051
[4] Girard, J.-Y.: The System F of Variable Types, Fifteen Years Later.Theoretical Computer Science, 45, 159–192 (1986). · Zbl 0623.03013 · doi:10.1016/0304-3975(86)90044-7
[5] Girard, J.-Y.: Linear Logic and Parallelism. Proc. School on Semantics of Parallelism, IAC, CNR, Roma, September 1986.
[6] Girard, J.-Y.: Linear Logic.Theoretical Computer Science, 50, 1–102 (1987). · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[7] Girard, J.-Y., and Lafont, Y.: Linear Logic and Lazy Computation. In.Tapsoft ’87. LNCS 250, pp. 52–66, Springer Verlag, 1987. · Zbl 0647.03016
[8] Hu, S.-T.:Introduction to General Topology. Holden-Day, 1966. · Zbl 0132.17602
[9] Kuratowski, K.:Introduction to Set Theory and Topology. Pergamon Press, 1977. · Zbl 0367.28001
[10] Shoenfield, J. R.:Mathematical Logic. Addison-Wesley, 1967. · Zbl 0155.01102
[11] Takeuti, G.:Proof Theory (2nd edn), North Holland, 1987. · Zbl 0609.03019
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.