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