Z. M. Ariola, H. Herbelin & A. Sabry (2009):
A type-theoretic foundation of delimited continuations.
Higher-Order and Symbolic Computation 22(3),
pp. 233–273.
Available at http://dx.doi.org/10.1007/s10990-007-9006-0.
L. Buisman (Postniece) & R. Goré (2007):
A cut-free sequent calculus for bi-intuitionistic logic.
In: N. Olivetti: Proc. of 16th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007 (Aix en Provence, July 2007),
Lect. Notes in Comput. Sci. 4548.
Springer,
pp. 90–106.
Available at http://dx.doi.org/10.1007/978-3-540-73099-6_9.
T. Crolard (2004):
A formulae-as-types interpretation of subtractive logic.
J. of Log. and Comput. 14(4),
pp. 529–570.
Available at http://dx.doi.org/10.1093/logcom/14.4.529.
P.-L. Curien & H. Herbelin (2000):
The duality of computation.
In: Proc. of 5th Int. Conf. on Functional Programming, ICFP '00 (Montreal, Sept. 2000).
ACM Press,
pp. 233–243.
Available at http://doi.acm.org/10.1145/351240.351262.
R. Goré, L. Postniece & A. Tiu (2008):
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.
In: C. Areces & R. Goldblatt: Advances in Modal Logic 7.
College Publications,
pp. 43–66.
Available at http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
L. Pinto & T. Uustalu (2009):
Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents.
In: M. Giese & A. Waaler: Proc. of 18th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 (Oslo, July 2009),
Lect. Notes in Artif. Intell. 5607.
Springer,
pp. 295–309.
Available at http://dx.doi.org/10.1007/978-3-642-02716-1_22.
L. Postniece (2009):
Deep Inference in Bi-intuitionistic Logic.
In: H. Ono, M. Kanazawa & R. Queiroz: Proc. of 16th Int. Wksh. on Logic, Language, Information and Computation, WoLLiC 2009 (Tokyo, June 2009),
Lect. Notes in Artif. Intell. 5514.
Springer,
pp. 320–334.
Available at http://dx.doi.org/10.1007/978-3-642-02261-6_26.
C. Rauszer (1974):
A formalization of the propositional calculus of H-B logic.
Studia Logica 33(1),
pp. 23–34.
Available at http://dx.doi.org/10.1007/bf02120864.
C. Rauszer (1977):
Applications of Kripke models to Heyting-Brouwer logic.
Studia Logica 36(1–2),
pp. 61–71.
Available at http://dx.doi.org/10.1007/bf02121115.
J. Reed & F. Pfenning (2009):
Intuitionistic letcc via labelled deduction.
Electron. Notes in Theor. Comput. Sci. 231,
pp. 91–111.
Available at http://dx.doi.org/10.1016/j.entcs.2009.02.031.