@inproceedings(Asai2002,
 author       = "Kenichi Asai",
 year         = "2002",
 title        = "Online partial evaluation for shift and reset",
 editor       = "Peter Thiemann",
 booktitle    = "Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '02), Portland, Oregon, USA, January 14-15, 2002",
 publisher    = "ACM",
 pages        = "19--30",
 doi          = "10.1145/503032.503034",
)
@inproceedings(Asai2004,
 author       = "Kenichi Asai",
 year         = "2004",
 title        = "Offline partial evaluation for shift and reset",
 editor       = "Nevin Heintze and Peter Sestoft",
 booktitle    = "Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulatiog, 2004, Verona, Italy, August 24-25, 2004",
 publisher    = "ACM",
 pages        = "3--14",
 doi          = "10.1145/1014007.1014009",
)
@inproceedings(BergerS1991,
 author       = "Ulrich Berger and Helmut Schwichtenberg",
 year         = "1991",
 title        = "An Inverse of the Evaluation Functional for Typed lambda-calculus",
 booktitle    = "Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, 1991, Amsterdam, The Netherlands",
 publisher    = "IEEE Computer Society",
 pages        = "203--211",
 doi          = "10.1109/LICS.1991.151645",
)
@inproceedings(BiernackaB2009,
 author       = "Malgorzata Biernacka and Dariusz Biernacki",
 year         = "2009",
 title        = "Context-based proofs of termination for typed delimited-control operators",
 booktitle    = "Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming",
 series       = "PPDP '09",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "289--300",
 doi          = "10.1145/1599410.1599446",
)
@inproceedings(CCoquand1993,
 author       = "Catarina Coquand",
 year         = "1993",
 title        = "From Semantics to Rules: A Machine Assisted Analysis",
 booktitle    = "CSL '93",
 series       = "Lecture Notes in Computer Science",
 volume       = "832",
 publisher    = "Springer",
 pages        = "91--105",
 doi          = "10.1007/BFb0049326",
)
@incollection(Danvy1999,
 author       = "Olivier Danvy",
 year         = "1999",
 title        = "Type-Directed Partial Evaluation",
 editor       = "John Hatcliff and Torben Mogensen and Peter Thiemann",
 booktitle    = "Partial Evaluation",
 series       = "Lecture Notes in Computer Science",
 volume       = "1706",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "367--411",
 doi          = "10.1007/3-540-47018-2\_16",
)
@techreport(DanvyF1989,
 author       = "Olivier Danvy and Andrzej Filinski",
 year         = "1989",
 title        = "A Functional Abstraction of Typed Contexts",
 type         = "Technical Report",
 institution  = "Computer Science Department, University of Copenhagen",
 note         = "DIKU Rapport 89/12",
)
@inproceedings(DanvyF1990,
 author       = "Olivier Danvy and Andrzej Filinski",
 year         = "1990",
 title        = "Abstracting Control",
 booktitle    = "LISP and Functional Programming",
 pages        = "151--160",
 doi          = "10.1145/91556.91622",
)
@article(DanvyF1992,
 author       = "Olivier Danvy and Andrzej Filinski",
 year         = "1992",
 title        = "Representing Control: A Study of the {CPS} Transformation",
 journal      = "Mathematical Structures in Computer Science",
 volume       = "2",
 number       = "4",
 pages        = "361--391",
 doi          = "10.1017/S0960129500001535",
)
@phdthesis(FilinskiThesis,
 author       = "Andrzej Filinski",
 year         = "1996",
 title        = "Controlling Effects",
 school       = "School of Computer Science, Carnegie Mellon University",
 note         = "Technical Report CMU-CS-96-119 (144pp.)",
)
@article(GregoireL2002,
 author       = "Benjamin Gr{\'e}goire and Xavier Leroy",
 year         = "2002",
 title        = "A compiled implementation of strong reduction",
 journal      = "SIGPLAN Not.",
 volume       = "37",
 number       = "9",
 pages        = "235--246",
 doi          = "10.1145/583852.581501",
)
@article(Ilik2010,
 author       = "Danko Ilik",
 year         = "2012",
 title        = "Delimited control operators prove Double-negation Shift",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "163",
 number       = "11",
 pages        = "1549 -- 1559",
 doi          = "10.1016/j.apal.2011.12.008",
)
@article(Ilik2011,
 author       = "Danko Ilik",
 year         = "2013",
 title        = "Continuation-passing style models complete for intuitionistic logic",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "164",
 number       = "6",
 pages        = "651 -- 663",
 doi          = "10.1016/j.apal.2012.05.003",
)
@article(IlikLH2010,
 author       = "Danko Ilik and Gyesik Lee and Hugo Herbelin",
 year         = "2010",
 title        = "Kripke models for classical logic",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "161",
 number       = "11",
 pages        = "1367 -- 1378",
 doi          = "10.1016/j.apal.2010.04.007",
 note         = "Special Issue: Classical Logic and Computation (2008)",
)
@article(Kameyama2007,
 author       = "Yukiyoshi Kameyama",
 year         = "2007",
 title        = "Axioms for control operators in the CPS hierarchy",
 journal      = "Higher Order Symbol. Comput.",
 volume       = "20",
 number       = "4",
 pages        = "339--369",
 doi          = "10.1007/s10990-007-9009-x",
)
@inproceedings(KameyamaTanaka2010,
 author       = "Yukiyoshi Kameyama and Asami Tanaka",
 year         = "2010",
 title        = "Equational axiomatization of call-by-name delimited control",
 booktitle    = "Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming",
 series       = "PPDP '10",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "77--86",
 doi          = "10.1145/1836089.1836100",
)
@book(TroelstraVD1,
 author       = "A. S. Troelstra and D. {van Dalen}",
 year         = "1988",
 title        = "Constructivism in mathematics. {V}ol. {I}",
 series       = "Studies in Logic and the Foundations of Mathematics",
 volume       = "121",
 publisher    = "North-Holland Publishing Co.",
 address      = "Amsterdam",
 doi          = "10.1016/S0049-237X(09)70523-3",
 note         = "An introduction",
)
@inproceedings(TsushimaAsai2009,
 author       = "Kanae Tsushima and Kenichi Asai",
 year         = "2009",
 title        = "Towards Type-Directed Partial Evaluation for Shift and Reset",
 booktitle    = "Informal proceedings of the 2009 Workshop on Normalization by Evaluation",
 address      = "Los Angeles, California",
 pages        = "57--64",
)