Proof theory in the abstract

Benton, 1993, Linear lambda-calculus and categorical models revisited, vol. 702, 61

Benton, 1993, A term calculus for intuitionistic linear logic, vol. 664, 75

G.M. Bierman, On intuitionistic linear logic, Ph.D. Thesis, Computer Laboratory, Cambridge University, 1993.

G.M. Bierman, What is a categorical model of linear logic? in: Proc. Second Internat. Conf. Typed Lambda Calculi and Applications, TCLA’ in Computer Science, Springer, Berlin, 1995, pp. 78–93.

Blute, 1996, Natural deduction and coherence for weakly distributive categories, J. Pure Appl. Algebra, 113, 229, 10.1016/0022-4049(95)00159-X

Burr, 1999, Concepts and aims of functional interpretations, 205

Cockett, 1992, Weakly distributive categories, vol. 177, 45

Cockett, 1997, Weakly distributive categories, J. Pure Appl. Algebra, 114, 133, 10.1016/0022-4049(95)00160-3

Crole, 1993

Danos, 1995, LKT and LKQ: sequent calculi for second order logic based upon dual linear decomposition of classical implication, vol. 222, 211

de Paiva, 1989, The Dialectica categories, vol. 92, 47

V.C.V. de Paiva, The Dialectica categories, Ph.D. Thesis, Dept. Pure Mathematics and Mathematical Statistics, University of Cambridge, 1988, published as Computer Laboratory Tech. Report 213, 1990.

V.C.V. de Paiva, A Dialectica model of the Lambek calculus, Proc. of the 8th Amsterdam Colloq., 1991, pp. 445–461.

Diller, 1979, Functional interpretation of Heyting's Arithmetic in all finite types, Nieuw Arch. Wiskunde, 27, 70

Diller, 1974, Eine Variante zur Dialectica-interpretation der Heyting-Arithmetik endlicher Typen, Arch. Math. Logik Grundlag., 16, 49, 10.1007/BF02025118

1995, vol. III

1990, vol. II

J.-Y. Girard, Interprétation fonctionelle et élimination des coupures de l'arithmetique d'ordre supéreure, Ph.D. Thesis, Paris, 1971.

Girard, 1987, Linear Logic, Theoret. Comput. Sci., 50, 1, 10.1016/0304-3975(87)90045-4

Girard, 1991, A new constructive logic, Math. Struct. Comput. Sci., 1, 255, 10.1017/S0960129500001328

Girard, 1993, On the unity of logic, Ann. Pure Appl. Logic, 59, 201, 10.1016/0168-0072(93)90093-S

Girard, 1988

Gödel, 1958, Über eine bischer noch nicht benütze Erweiterung des finiten Standpunktes, Dialectica, 12, 280, 10.1111/j.1746-8361.1958.tb01464.x

Hofmann, 1997, Continuation models are universal for λμ-calculus, 387

Hyland, 1993, Full intuitionistic linear logic, Ann. Pure Appl. Logic, 64, 273, 10.1016/0168-0072(93)90146-5

Jacobs, 1999

Y. Lafont, Logiques, categories et machines, Ph.D. Thesis, University of Paris VII, 1988.

Lambek, 1993, From categorial grammar to bilinear logic, 207

Lambek, 1995, Bilinear logic, vol. 222, 43

Lambek, 1986

Martin-Löf, 1984

M. Parigot, λμ-calculus: an algorithmic interpretation of classical natural deduction, Proc. Internat. Conf. on Logic Programming and Automated Reasoning. St. Petersburg, 1992.

J. Power, Premonoidal categories as categories with algebraic structure, Theoret. Comput. Sci. (2001), to appear.

Power, 1997, Premonoidal categories and notions of computation, Math. Struct. Comput. Sci., 7, 453, 10.1017/S0960129597002375

H. Schellinx, The noble art of linear decorating, Ph.D. Thesis, University of Amsterdam, 1994.

Seely, 1989, Linear logic, *-autonomous categories and cofree coalgebras, vol. 92, 371

Selinger, 2001, Control categories and duality, Math. Struct. Comput. Sci., 11, 207, 10.1017/S096012950000311X

Shoenfield, 1967

Szabo, 1975, Polycategories, Comm. Algebra, 3, 663, 10.1080/00927877508822067

Taylor, 1999

H. Thielecke, Categorical semantics of continuation passing style, Ph.D. Thesis, University of Edinburgh, 1997.

Troelstra, 1973

Troelstra, 1992, vol. 29

Troelstra, 1996

C. Urban, Classical logic and computation, Ph.D. Thesis, University of Cambridge, 2000.

Urban, 1999, Strong normalisation of cut-elimination in classical logic, vol. 1581, 365

Urban, 2000, Strong normalisation of cut-elimination in classical logic, Fund. Inform., 45, 123

J. van Oosten, Realizability: a historical essay, Math. Struct. Comput. Sci. (2001), to appear.