Z.M. Ariola & H. Herbelin (2003):
Minimal classical logic and control operators.
In: ICALP,
pp. 871–885,
doi:10.1007/3-540-45061-0_68.
A. Bucciarelli, T. Ehrhard & G. Manzonetto (2007):
Not Enough Points Is Enough.
In: CSL,
LNCS 4646,
pp. 298–312,
doi:10.1007/978-3-540-74915-8_24.
P.-L Curien & H. Herbelin (2000):
The duality of computation.
In: ACM SIGPLAN International Conference on Functional Programming,
pp. 233–243,
doi:10.1145/351240.351262.
J. Czermak (1977):
A Remark on Gentzen's Calculus of Sequents.
Notre Dame Journal of Formal Logic 18(3),
pp. 471–474,
doi:10.1305/ndjfl/1093888021.
V. Danos, J.-B. Joinet & H. Schellinx (1995):
LKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication.
In: J.-Y. Girard, Y. Lafont & L. Regnier: Advances in linear logic,
London Math. Society Lecture Note Series 222.
R. David & W. Py (2001):
λμ-Calculus and Böhm's Theorem.
J. Symb. Log. 66(1),
pp. 407–413,
doi:10.2307/2694930.
P. De Groote (1994):
On the relation between the λμ-calculus and the syntactic theory of sequential control.
In: LPAR,
pp. 31–43,
doi:10.1007/3-540-58216-9_27.
P. De Groote (1995):
A Simple Calculus of Exception Handling.
In: TLCA,
pp. 201–215.
P. De Groote (1998):
An environment machine for the λμ-calculus.
Math. Struct. Comp. Sci. 8(6),
pp. 637–669,
doi:10.1017/S0960129598002667.
M. Felleisen & R. Hieb (1992):
The Revised Report on the Syntactic Theories of Sequential Control and State.
Theor. Comput. Sci. 103,
pp. 235–271,
doi:10.1016/0304-3975(92)90014-7.
G. Gentzen (1935):
Investigations into logical deduction.
J.-Y. Girard (1986):
The system F of variable types, fifteen years later.
Theor. Comput. Sci. 45,
pp. 159–192,
doi:10.1016/0304-3975(86)90044-7.
J.-Y. Girard (1991):
A new constructive logic: Classical Logic.
Math. Struct. in Comp. Sci. 1(3),
pp. 255–296,
doi:10.1017/S0960129500001328.
T. Griffin (1990):
A Formulae-as-Types Notion of Control.
In: POPL,
pp. 47–58,
doi:10.1145/96709.96714.
M. Hofmann & T. Streicher (1997):
Continuation Models are Universal for lambda-mu-Calculus.
In: LICS,
pp. 387–395,
doi:10.1109/LICS.1997.614964.
W.A. Howard (1980):
The formulae-as-types notion of construction.
In: J.R. Hindley & J.P. Seldin: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,
pp. 479–490.
J.W. Klop & R.C. de Vrijer (1989):
Unique normal forms for lambda calculus with surjective pairing.
Information and Computation 2,
pp. 97–113,
doi:10.1016/0890-5401(89)90014-X.
J.-L. Krivine (2001):
Typed lambda-calculus in classical Zermelo-Frænkel set theory.
Arch. Math. Log. 40(3),
pp. 189–205,
doi:10.1007/s001530000057.
Y. Lafont, B. Reus & T. Streicher (1993):
Continuations Semantics or Expressing Implication by Negation.
Technical Report 9321.
Ludwig-Maximilians-Universitat, Munchen.
Technical Report.
O. Laurent (2003):
Krivine's abstract machine and the lambda mu-calculus (an overview).
Unpublished.
O. Laurent (2003):
Polarized proof-nets and lambda-mu calculus.
Theor. Comput. Sci. 290(1),
pp. 161–188,
doi:10.1016/S0304-3975(01)00297-3.
O. Laurent (2011):
Intuitionistic Dual-intuitionistic Nets.
J. Log. Comput. 21(4),
pp. 561–587,
doi:10.1093/logcom/exp044.
O. Laurent & L. Regnier (2003):
About Translations of Classical Logic into Polarized Linear Logic.
In: LICS,
pp. 11–20,
doi:10.1109/LICS.2003.1210040.
S. Lengrand (2003):
Call-by-value, call-by-name, and strong normalization for the classical sequent calculus.
Elec. Notes in Theor. Comp. Sci. 86,
doi:10.1016/S1571-0661(05)82619-2.
WRS.
T. Low & T. Streicher (2006):
Universality Results for Models in Locally Boolean Domains.
In: CSL,
pp. 456–470,
doi:10.1007/11874683_30.
M. Parigot (1992):
λμ-calculus: An Algorithmic Interpretation of Classical Natural Deduction.
In: LPAR,
pp. 190–201,
doi:10.1007/BFb0013061.
D. Prawitz (1965):
Natural Deduction - a proof theoretical study.
Almqvist & Wiksell,
Stokholm.
B. Reus & T. Streicher (1998):
Classical Logic, Continuation Semantics and Abstract Machines.
J. Funct. Program. 8(6),
pp. 543–572,
doi:10.1017/S0956796898003141.
P. Selinger (2001):
Control categories and duality: on the categorical semantics of the lambda-mu calculus.
Math. Struct. in Comp. Sci. 11,
pp. 207–260,
doi:10.1017/S096012950000311X.
eptcs@eptcs.org