@article(Anderson76,
 author       = {B. Anderson},
 year         = {1976},
 title        = {The Samefringe Problem},
 journal      = {SIGART Bull.},
 volume       = {60},
 pages        = {4--4},
)
@inproceedings(Anton10,
 author       = {K. Anton and P. Thiemann},
 year         = {2010},
 title        = {Towards Deriving Type Systems and Implementations for Coroutines},
 editor       = {Kazunori Ueda},
 booktitle    = {Programming Languages and Systems -- 8th Asian Symposium, APLAS 2010},
 series       = {LNCS},
 volume       = {6461},
 publisher    = {Springer},
 address      = {Shanghai, China},
 pages        = {63--79},
 doi          = {10.1007/ 978-3-642-17164-2\_6},
)
@inproceedings(Berardi94b,
 author       = {F. Barbanera and S. Berardi},
 year         = {1994},
 title        = {{Extracting Constructive Content from Classical Logic via Control-like Reductions}},
 booktitle    = {LNCS},
 volume       = {662},
 publisher    = {Springer-Verlag},
 pages        = {47--59},
 doi          = {10.1.1.120.386},
)
@article(Bellin14,
 author       = {G. Bellin and A. Menti},
 year         = {2014},
 title        = {{On the $\pi$-calculus and Co-intuitionistic Logic. Notes on Logic for Concurrency and $\lambda$P Systems}},
 journal      = {Fundamenta Informaticae},
 volume       = {130},
 number       = {1},
 pages        = {21--65},
 doi          = {10.3233/FI-2014-981},
)
@article(Biernacka07,
 author       = {M. Biernacka and O. Danvy},
 year         = {2007},
 title        = {{A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines}},
 journal      = {Theoretical Computer Science},
 volume       = {375},
 doi          = {10.1016/j.tcs.2006.12.028},
)
@article(Biernacki06,
 author       = {D. Biernacki and O. Danvy and C. Shan},
 year         = {2006},
 title        = {On the Static and Dynamic Extents of Delimited Continuations},
 journal      = {Science of Computer Programming},
 volume       = {60},
 number       = {3},
 pages        = {274--297},
 doi          = {10.1016/j.scico.2006.01.002},
)
@mastersthesis(Brede09,
 author       = {N. Brede},
 year         = {2009},
 title        = {{$\lambda\mu $PRL - A Proof Refinement Calculus for Classical Reasoning in Computational Type Theory}},
 school       = {University of Potsdam},
 url          = {http://www.cs.uni-potsdam.de/~brede},
)
@article(Clint73,
 author       = {M. Clint},
 year         = {1973},
 title        = {{Program proving: Coroutines}},
 journal      = {Acta Informatica},
 volume       = {2},
 number       = {1},
 pages        = {50--63},
 doi          = {10.1007/BF00571463},
)
@article(Conway63,
 author       = {M. E. Conway},
 year         = {1963},
 title        = {{Design of a separable transition-diagram compiler}},
 journal      = {Commun. ACM},
 volume       = {6},
 number       = {7},
 pages        = {396--408},
 doi          = {10.1145/366663.366704},
)
@misc(Crolard96,
 author       = {T. Crolard},
 year         = {1996},
 title        = {{Extension de l'Isomorphisme de {C}urry-{H}oward au Traitement des Exceptions (application d'une {\'e}tude de la dualit{\'e} en logique intuitionniste)}},
 howpublished = {Th{\`e}se de Doctorat. Universit{\'e} Paris 7},
)
@article(Crolard98a,
 author       = {T. Crolard},
 year         = {1999},
 title        = {{A confluent lambda-calculus with a catch/throw mechanism}},
 journal      = {Journal of Functional Programming},
 volume       = {9},
 number       = {6},
 pages        = {625--647},
 doi          = {10.1017/S0956796899003512},
)
@article(Crolard01,
 author       = {T. Crolard},
 year         = {2001},
 title        = {{S}ubtractive {L}ogic},
 journal      = {Theoretical Computer Science},
 volume       = {254},
 number       = {1--2},
 pages        = {151--185},
 doi          = {10.1016/S0304-3975(99)00124-3},
)
@article(Crolard04,
 author       = {T. Crolard},
 year         = {2004},
 title        = {{A} {F}ormul{\ae}-as-{T}ypes {I}nterpretation of {S}ubtractive {L}ogic},
 journal      = {Journal of Logic and Computation},
 volume       = {14},
 number       = {4},
 pages        = {529--570},
 doi          = {10.1093/logcom/14.4.529},
)
@techreport(Crolard15,
 author       = {T. Crolard},
 year         = {2015},
 title        = {{A verified abstract machine for functional coroutines - Coq formalization}},
 type         = {Technical Report},
 institution  = {CEDRIC - Conservatoire National des Arts et M{\'e}tiers},
 url          = {http://cedric.cnam.fr/cpr/crolard/publications},
)
@inproceedings(Curien00,
 author       = {P.-L. Curien and H. Herbelin},
 year         = {2000},
 title        = {{The duality of computation.}},
 booktitle    = {Proceedings of the {ACM} SIGPLAN International Conference on Functional Programming ({ICFP}'00)},
 publisher    = {ACM Press},
 address      = {New York, USA},
 pages        = {233--243},
 doi          = {10.1145/351240.351262},
)
@book(Dahl72,
 author       = {O. J. Dahl and E. W. Dijkstra and C. A. R. Hoare},
 year         = {1972},
 title        = {{Structured programming}},
 publisher    = {Academic Press},
)
@article(Dahl66,
 author       = {O.-J. Dahl and K. Nygaard},
 year         = {1966},
 title        = {{SIMULA: an ALGOL-based simulation language}},
 journal      = {Commun. ACM},
 volume       = {9},
 number       = {9},
 pages        = {671--678},
 doi          = {10.1145/365813.365819},
)
@inproceedings(Danvy08,
 author       = {O. Danvy},
 year         = {2008},
 title        = {Defunctionalized Interpreters for Programming Languages},
 booktitle    = {Proceedings of the {ACM} SIGPLAN International Conference on Functional Programming (ICFP'08)},
 publisher    = {ACM Press},
 address      = {New York, USA},
 pages        = {131--142},
 doi          = {10.1145/1411204.1411206},
)
@article(Danvy07,
 author       = {{Danvy, editor}, O.},
 year         = {2007},
 title        = {{Special Issue on the Krivine Machine}},
 journal      = {Higher-Order and Symbolic Computation},
 volume       = {20},
 number       = {3},
 doi          = {10.1007/s10990-007-9021-1},
)
@article(Dybvig89,
 author       = {R. K. Dybvig and R. Hieb},
 year         = {1989},
 title        = {{Engines From Continuations}},
 journal      = {Comput. Lang},
 volume       = {14},
 number       = {2},
 pages        = {109--123},
 doi          = {10.1016/0096-0551(89)90018-0},
)
@article(Eades16,
 author       = {H. Eades and A. Stump and R. McCleeary},
 year         = {2016},
 title        = {Dualized simple type theory},
 journal      = {Submitted to Logical Methods in Computer Science},
)
@article(Fortune83,
 author       = {S. Fortune and D. Leivant and M. O'Donnell},
 year         = {1983},
 title        = {The Expressiveness of Simple and Second-Order Type Structures},
 journal      = {J. ACM},
 volume       = {30},
 number       = {1},
 pages        = {151--185},
 doi          = {10.1145/322358.322370},
)
@article(Wand86,
 author       = {D. P. Friedman and C. T. Haynes and M. Wand},
 year         = {1986},
 title        = {{Obtaining Coroutines with Continuations}},
 journal      = {Journal of Computer Languages},
 volume       = {11},
 number       = {3/4},
 pages        = {143--153},
 doi          = {10.1016/0096-0551(86)90007-X},
)
@article(Gore08,
 author       = {R. Gor{\'e} and L. Postniece},
 year         = {2010},
 title        = {{Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic}},
 journal      = {Journal of Logic and Computation},
 doi          = {10.1093/logcom/exn067},
)
@article(Gornemann71,
 author       = {S. G{\"o}rnemann},
 year         = {1971},
 title        = {{A logic stronger than intuitionism}},
 journal      = {The Journal of Symbolic Logic},
 volume       = {36},
 pages        = {249--261},
 doi          = {10.2307/2270260},
)
@article(Greussay76,
 author       = {P. Greussay},
 year         = {1976},
 title        = {An Iterative Lisp Solution to the Samefringe Problem},
 journal      = {SIGART Bull.},
 volume       = {59},
 pages        = {14--14},
 doi          = {10.1145/1045270.1045273},
)
@inproceedings(Griffin90,
 author       = {T. G. Griffin},
 year         = {1990},
 title        = {{A formul{\ae}-as-types notion of control}},
 booktitle    = {Conference Record of the 17th Annual ACM Symposium on Principles of Programming Langages},
 pages        = {47--58},
 doi          = {10.1145/96709.96714},
)
@article(deGroote98,
 author       = {P. de Groote},
 year         = {1998},
 title        = {{An environment machine for the lambda-mu-calculus.}},
 journal      = {Mathematical Structure in Computer Science},
 volume       = {8},
 pages        = {637--669},
 doi          = {10.1017/S0960129598002667},
)
@incollection(deGroote01,
 author       = {P. de Groote},
 year         = {2001},
 title        = {Strong Normalization of Classical Natural Deduction with Disjunction},
 editor       = {S. Abramsky},
 booktitle    = {Typed Lambda Calculi and Applications},
 series       = {LNCS},
 volume       = {2044},
 publisher    = {Springer},
 pages        = {182--196},
 doi          = {10.1007/3-540-45413-6\_17},
)
@article(Grzegorczyk64,
 author       = {A. Grzegorczyk},
 year         = {1964},
 title        = {{A philosophically plausible formal interpretation of intuitionistic logic.}},
 journal      = {Nederl. Akad. Wet., Proc., Ser. A},
 volume       = {67},
 pages        = {596--601},
 doi          = {10.2307/2271877},
)
@article(MacQueen93,
 author       = {R. Harper and B. F. Duba and D. MacQueen},
 year         = {1993},
 title        = {Typing first-class continuations in {ML}},
 journal      = {Journal of Functional Programming},
 volume       = {3},
 number       = {4},
 pages        = {465--484},
 doi          = {10.1017/S095679680000085X},
)
@techreport(Kashima91,
 author       = {R. Kashima},
 year         = {1991},
 title        = {{Cut-Elimination for the intermediate logic CD}},
 type         = {Research Report on Information Sciences},
 number       = {C100},
 institution  = {Institute of Technology},
 address      = {Tokyo},
)
@inproceedings(Kimura09,
 author       = {D. Kimura and M. Tatsuta},
 year         = {2009},
 title        = {Dual Calculus with Inductive and Coinductive Types},
 editor       = {Ralf Treinen},
 booktitle    = {Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Bras\'{\i}lia, Brazil},
 series       = {LNCS},
 volume       = {5595},
 publisher    = {Springer},
 pages        = {224--238},
 doi          = {10.1007/978-3-642-02348-4\_16},
)
@book(Knuth97,
 author       = {D. E. Knuth},
 year         = {1997},
 title        = {{The Art of Computer Programming, Volume I: Fundamental Algorithms}},
 edition      = {3rd edition},
 publisher    = {Addison-Wesley},
)
@article(Krivine94,
 author       = {J.-L. Krivine},
 year         = {1994},
 title        = {{Classical logic, storage operators and second order $\lambda$-calculus}},
 journal      = {Ann. of Pure and Appl. Logic},
 volume       = {68},
 pages        = {53--78},
 doi          = {10.1016/0168-0072(94)90047-7},
)
@article(Leivant02,
 author       = {D. Leivant},
 year         = {2002},
 title        = {{Intrinsic reasoning about functional programs {I}: first order theories}},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {114},
 number       = {1-3},
 pages        = {117--153},
 doi          = {10.1016/S0168-0072(01)00078-1},
)
@article(Lopez-Escobar83,
 author       = {Lopez-Escobar, E. G. K.},
 year         = {1983},
 title        = {{A Second Paper ``On the Interpolation Theorem for the Logic of Constant Domains"}},
 journal      = {The Journal of Symbolic Logic},
 volume       = {48},
 number       = {3},
 pages        = {595--599},
 doi          = {10.2307/2273451},
 url          = {http://www.jstor.org/stable/2273451},
)
@book(Marlin80,
 author       = {C. D. Marlin},
 year         = {1980},
 title        = {{Coroutines: A Programming Methodology, a Language Design and an Implementation}},
 publisher    = {Springer-Verlag New York, Inc.},
 address      = {Secaucus, NJ, USA},
 doi          = {10.1007/3-540-10256-6},
)
@article(McCarthy77,
 author       = {J. McCarthy},
 year         = {1977},
 title        = {Another SAMEFRINGE},
 journal      = {SIGART Bull.},
 volume       = {61},
 pages        = {4--4},
)
@article(Mints13,
 author       = {G. Mints and G. Olkhovikov and A. Urquhart},
 year         = {2013},
 title        = {Failure of Interpolation in Constant Domain Intuitionistic Logic},
 journal      = {The Journal of Symbolic Logic},
 volume       = {78},
 pages        = {937--950},
 doi          = {10.2178/jsl.7803120},
 url          = {http://journals.cambridge.org/article_S0022481200126672},
)
@techreport(Moura04a,
 author       = {A. L. de Moura and R. Ierusalimschy},
 year         = {2004},
 title        = {{Revisiting Coroutines}},
 type         = {MCC},
 number       = {15/04},
 institution  = {PUC-Rio},
 address      = {Rio de Janeiro, RJ},
 doi          = {10.1145/1462166.1462167},
)
@article(Moura04,
 author       = {A. L. de Moura and N. Rodriguez and R. Ierusalimschy},
 year         = {2004},
 title        = {{Coroutines in Lua}},
 journal      = {Journal of Universal Computer Science},
 volume       = {10},
 number       = {7},
 pages        = {910--925},
 doi          = {10.3217/jucs-010-07-0910},
)
@techreport(Murthy91b,
 author       = {C. R. Murthy},
 year         = {1991},
 title        = {{Classical proofs as programs: How, when, and why}},
 type         = {Technical Report},
 number       = {91-1215},
 institution  = {Cornell University, Department of Computer Science},
)
@inproceedings(Parigot94,
 author       = {M. Parigot},
 year         = {1993},
 title        = {{Strong normalization for second order classical natural deduction}},
 booktitle    = {Proceedings of the eighth annual {IEEE} symposium on logic in computer science},
 pages        = {39--46},
 doi          = {10.1109/LICS.1993.287602},
)
@article(Pinto09,
 author       = {L. Pinto and T. Uustalu},
 year         = {2009},
 title        = {{Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents}},
 journal      = {Automated Reasoning with Analytic Tableaux and Related Methods},
 pages        = {295--309},
 doi          = {10.1007/978-3-642-02716-1\_22},
)
@inproceedings(Pinto10,
 author       = {L. Pinto and T. Uustalu},
 year         = {2010},
 title        = {{Relating Sequent Calculi for Bi-intuitionistic Propositional Logic}},
 editor       = {S. van Bakel and S. Berardi and U. Berger},
 booktitle    = {Proc. of the 3rd Workshop on Classical logic and Computation},
 organization = {Masarykova Univ.},
 pages        = {68--85},
 doi          = {10.4204/EPTCS.47.7},
)
@article(Prenner71,
 author       = {C. J. Prenner},
 year         = {1971},
 title        = {The Control Structure Facilities of ECL},
 journal      = {SIGPLAN Not.},
 volume       = {6},
 number       = {12},
 pages        = {104--112},
 doi          = {10.1145/800006.807990},
)
@article(Pym00,
 author       = {D. Pym and E. Ritter and L. Wallen},
 year         = {2000},
 title        = {{On the intuitionistic force of classical search}},
 journal      = {Theoretical Computer Science},
 volume       = {232(1-2)},
 pages        = {299--333},
 doi          = {10.1016/S0304-3975(99)00178-4},
)
@inproceedings(Rauszer74,
 author       = {C. Rauszer},
 year         = {1974},
 title        = {{Semi-Boolean algebras and their applications to intuitionistic logic with dual operations}},
 booktitle    = {Fundamenta Mathematicae},
 volume       = {83},
 pages        = {219--249},
)
@incollection(Rauszer80,
 author       = {C. Rauszer},
 year         = {1980},
 title        = {{An algebraic and {K}ripke-style approach to a certain extension of intuitionistic logic}},
 booktitle    = {Dissertationes Mathematicae},
 volume       = {167},
 publisher    = {Institut Math{\'e}matique de l'Acad{\'e}mie Polonaise des Sciences},
 pages        = {1--67},
)
@inproceedings(Rehof94,
 author       = {N. J. Rehof and S{\o}rensen, M. H.},
 year         = {1994},
 title        = {{The $\lambda_\Delta$-calculus}},
 booktitle    = {Theoretical Aspects of Computer Software},
 series       = {LNCS},
 volume       = {542},
 publisher    = {Springer-Verlag},
 pages        = {516--542},
 doi          = {10.1007/3-540-57887-0\_113},
)
@inproceedings(Reppy95,
 author       = {J. H. Reppy},
 year         = {1995},
 title        = {First-class Synchronous Operations},
 booktitle    = {Proceedings of the International Workshop on Theory and Practice of Parallel Programming},
 series       = {LNCS},
 volume       = {907},
 publisher    = {Springer-Verlag},
 address      = {London, UK},
 pages        = {235--252},
 doi          = {10.1007/BFb0026573},
)
@article(Shimura94,
 author       = {T. Shimura and R. Kashima},
 year         = {1994},
 title        = {{Cut-Elimination Theorem for the Logic of Constant Domains}},
 journal      = {Math. Log. Q},
 volume       = {40},
 pages        = {153--172},
 doi          = {10.1002/malq.19940400203},
)
@techreport(Strachey74,
 author       = {C. Strachey and C. P. Wadsworth},
 year         = {1974},
 title        = {Continuations: A Mathematical Semantics for Handling Full Jumps},
 type         = {Technical Monograph},
 number       = {PRG-11},
 institution  = {Oxford University Computing Laboratory, Programming Research Group},
 address      = {Oxford, England},
 note         = {Reprinted in Higher-Order and Symbolic Computation 13(1/2):135--152, 2000, with a foreword~\cite{Wadsworth00}},
)
@article(Streicher98,
 author       = {T. Streicher and B. Reus},
 year         = {1998},
 title        = {{Classical Logic, Continuation Semantics and Abstract Machines}},
 journal      = {Journal of Functional Programming},
 volume       = {8},
 number       = {6},
 pages        = {543--572},
 doi          = {10.1017/S0956796898003141},
)
@misc(Open97,
 author       = {{The Open Group}},
 year         = {1997},
 title        = {{The {S}ingle {UNIX} {S}pecification, {V}ersion 2}},
 url          = {http://www.UNIX-systems.org/online.html},
)
@book(Troelstra73,
 author       = {A. S. Troelstra},
 year         = {1973},
 title        = {{Metamathematical Investigation of Intuitionistic Arithmetic and Analysis}},
 series       = {Lecture Notes in Mathematics},
 volume       = {344},
 publisher    = {Springer-Verlag},
 address      = {Berlin},
 doi          = {10.1007/BFb0066742},
)
@article(Wadsworth00,
 author       = {C. P. Wadsworth},
 year         = {2000},
 title        = {Continuations revisited},
 journal      = {Higher-Order and Symbolic Computation},
 volume       = {13},
 number       = {1/2},
 pages        = {131--133},
 doi          = {10.1023/A:1010074329461},
)
@book(Wirth80,
 author       = {N. Wirth and Mincer-Daszkiewicz, J.},
 year         = {1980},
 title        = {{Modula-2}},
 publisher    = {ETH Zurich, Schweiz},
 doi          = {10.3929/ethz-a-000189918},
)