P.-L. Curien & H. Herbelin (2000):
The duality of computation.
In: M. Odersky & P. Wadler: ICFP '00,
SIGPLAN Notices 35.
ACM,
pp. 233–243.
Available at http://doi.acm.org/10.1145/351240.351262.
P.-L. Curien & G. Munch-Maccagnoni (2010):
The Duality of Computation under Focus.
In: C.S. Calude & V. Sassone: TCS 2010,
IFIP Advances in Information and Communication Technology 323.
Springer,
pp. 165–181.
Available at http://dx.doi.org/10.1007/978-3-642-15240-5_13.
V. Danos, J.-B. Joinet & H. Schellinx (1997):
A New Deconstructive Logic: Linear Logic.
J. Symb. Log. 62(3),
pp. 755–807.
Available at http://dx.doi.org/10.2307/2275572.
P. Dehornoy & V. van Oostrom (2008):
Z, Proving Confluence by Monotonic Single-Step Upperbound Functions.
In: Logical Models of Reasoning and Computation (LMRC-08).
J. Espírito Santo, R. Matthes, K. Nakazawa & L. Pinto (2013):
Monadic translation of classical sequent calculi.
Mathematical Structures in Computer Science 23(6),
pp. 1111–1162.
Available at http://dx.doi.org/10.1017/S0960129512000436.
J-Y. Girard (1991):
A new constructive logic: classic logic.
Mathematical Structures in Computer Science 1(3),
pp. 255–296.
Available at http://dx.doi.org/10.1017/S0960129500001328.
J-Y. Girard, Y. Lafont & P. Taylor (1989):
Proofs and Types.
Cambridge University Press.
J. Hatcliff & O. Danvy (1994):
A generic account of continuation-passing styles.
In: H.-J. Boehm, B. Lang & D.M. Yellin: POPL'94.
ACM,
pp. 458–471.
Available at http://doi.acm.org/10.1145/174675.178053.
H. Herbelin (2005):
C'est maintenant qu'on calcule.
Habilitation Thesis.
P. Levy (2006):
Call-by-push-value: decomposing call-by-value and call-by-name.
Higher Order and Symbolic Computation 19(4),
pp. 377–414.
Available at http://dx.doi.org/10.1007/s10990-006-0480-6.
G. Munch-Maccagnoni (2009):
Focalisation and Classical Realisability.
In: E. Grädel & R. Kahle: CSL 2009,
LNCS 5771.
Springer,
pp. 409–423.
Available at http://dx.doi.org/10.1007/978-3-642-04027-6_30.
E. Polonovski (2004):
Strong normalization oføverline λμtilde07Eμ with explicit substitutions.
In: I. Walukiewicz: FoSSaCS 2004,
LNCS 2987.
Springer,
pp. 423–437.
Available at http://dx.doi.org/10.1007/978-3-540-24727-2_30.
V. van Oostrom & F. van Raamsdonk (1994):
Weak orthogonality implies confluence: the higher-order case.
In: A. Nerode & Y. Matiyasevich: LFCS '94,
LNCS 813.
Springer,
pp. 379–392.
Available at http://dx.doi.org/10.1007/3-540-58140-5_35.