The linear abstract machine. (English) Zbl 0648.68016

Linear logic [J.-Y. Girard, ibid. 50, 1-102 (1987; Zbl 0625.03037)] provides a refinement of functional programming and suggests a new implementation technique, with the following features: - a synthesis of strict and lazy evaluation, - a clean semantics of side effects, - no garbage collector.


68N01 General topics in the theory of software
68Q65 Abstract data types; algebraic specification
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03F05 Cut-elimination and normal-form theorems


Zbl 0625.03037
Full Text: DOI


[1] Cousineau, G.; Curien, P. L.; Mauny, M., The categorical abstract machine, (Jouannaud, J. P., Functional Programming Languages and Computer Architecture. Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, 201 (1985), Springer: Springer Berlin), 50-64 · Zbl 0592.68045
[2] Curien, P. L., Categorical combinatory logic, (Brauer, W., Proc. ICALP ’85. Proc. ICALP ’85, Lecture Notes in Computer Science, 194 (1985), Springer: Springer Berlin), 130-139 · Zbl 0587.03010
[3] Curien, P. L., Categorical Combinators, Sequential Algorithms and Functional Programming (1986), Pitman: Pitman London · Zbl 0643.68004
[4] (Szabo, E., The Collected Papers of Gerhard Gentzen (1969), North-Holland: North-Holland Amsterdam) · Zbl 0209.30001
[5] Girard, J. Y., Linear logic and parallelism, (Proc. School of Semantics of Parallelism, IAC (1986), CNR: CNR Roma) · Zbl 0357.02027
[6] Girard, J. Y., Linear logic, Theoret. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037
[7] Girard, J. Y.; Lafont, Y., Linear logic and lazy computation, (Proc. TAPSOFT ’87, Vol. 2. Proc. TAPSOFT ’87, Vol. 2, Lecture Notes in Computer Science, 250 (1987), Springer: Springer Berlin), 52-66 · Zbl 0647.03016
[8] Kelly, G. M., On MacLane’s conditions for coherence of natural associativities, J. Algebra, 1, 397-402 (1964) · Zbl 0246.18008
[9] Kleene, S. C., Introduction to Meta-mathematics (1952), North-Holland: North-Holland Amsterdam · Zbl 0047.00703
[10] Lafont, Y., Logiques, catégories et machines, (Thèse de Doctorat, 7 (1988), Université de Paris) · Zbl 0769.68060
[11] Lambek, J., Deductive systems and categories, Math. Systems Theory (1968) · Zbl 0176.28901
[12] Lambek, J., From lambda-calculus to cartesian closed categories, (Seldin, J. P.; Hindley, J. R., To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism (1980), Academic Press: Academic Press New York) · Zbl 0623.03014
[13] Lambek, J.; Scott, P. J., Introduction to Higher Order Categorical Logic, (Cambridge Studies in Advanced Mathematics (1986), Cambridge University Press: Cambridge University Press London) · Zbl 0596.03002
[14] MacLane, S., Categories for the Working Mathematician, (Graduate Texts in Mathematics, 5 (1971), Springer: Springer Berlin) · Zbl 0705.18001
[15] Martin-Löf, P., Intuitionistic Type Theory, (Studies in Proof Theory, Lecture Notes (1984), Bibliopolis: Bibliopolis Napoli) · Zbl 0571.03030
[16] Mauny, M.; Suarez, A., Implementing functional languages in the categorical abstract machine, (Proc. Lisp and Functional Programming Conf. (1986), ACM: ACM Boston, MA)
[17] Szabo, M. E., Algebra of Proofs, (Studies in Logic and the Foundations of Mathematics, 88 (1978), North-Holland: North-Holland Amsterdam) · Zbl 0532.03030
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.