cites.bib

@article{choi1975completely,
  title={Completely positive linear maps on complex matrices},
  author={Choi, Man-Duen},
  journal={Linear algebra and its applications},
  year={1975},
  publisher={Elsevier}
}

@article{jamiolkowski1972linear,
  title={Linear transformations which preserve trace and positive semidefiniteness of operators},
  author={Jamio{\l}kowski, Andrzej},
  journal={Reports on Mathematical Physics},
  year={1972},
  publisher={Elsevier}
}

@article{danos2007self,
  title={Self-assembling trees},
  author={Danos, V. and Krivine, J. and Tarissan, F.},
  journal={Electronic Notes in Theoretical Computer Science},
  pages={19--32},
  year={2007},
  publisher={Elsevier}
}

@article{plotkin1977lcf,
  title={LCF considered as a programming language},
  author={Plotkin, G.D.},
  journal={Theoretical Computer Science},
  pages={223--255},
  year={1977},
  publisher={Elsevier}
}

@article{plotkin2009handlers,
  title={Handlers of algebraic effects},
  author={Plotkin, G. and Pretnar, M.},
  journal={Programming Languages and Systems},
  pages={80--94},
  year={2009},
  publisher={Springer}
}

@article{bauer2012programming,
  title={Programming with Algebraic Effects and Handlers},
  author={Bauer, A. and Pretnar, M.},
  journal={arXiv preprint arXiv:1203.1539},
  year={2012}
}

@article{DBLP:journals/tcs/BergstraHT09,
  author    = {Jan A. Bergstra and
               Yoram Hirshfeld and
               J. V. Tucker},
  title     = {Meadows and the equational specification of division},
  journal   = {Theor. Comput. Sci.},
  volume    = {410},
  number    = {12-13},
  year      = {2009},
  pages     = {1261-1271},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2008.12.015},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/birthday/BergstraHT08,
  author    = {Jan A. Bergstra and
               Yoram Hirshfeld and
               John Tucker},
  title     = {Fields, Meadows and Abstract Data Types},
  booktitle = {Pillars of Computer Science},
  year      = {2008},
  pages     = {166-178},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78127-1_10}
}


@ARTICLE{Mcbride_applicativeprogramming,
    author = {Conor Mcbride and Ross Paterson},
    title = {Idioms : Applicative programming with effects},
    journal = {Journal of Functional Programming},
    year = {2007},
    volume = {18}
}

@inproceedings{DBLP:conf/csfw/MalacariaS12,
  author    = {Pasquale Malacaria and
               Fabrizio Smeraldi},
  title     = {The Thermodynamics of Confidentiality},
  booktitle = {CSF},
  year      = {2012},
  pages     = {280-290},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/CSF.2012.18},
}


@article{mellies2008categorical,
  title={Categorical semantics of linear logic},
  author={Melli{\`e}s, P.A.},
  journal={A para{\i}tre dans Panoramas et Syntheses, Soci{\'e}t{\'e} Math{\'e}matique de France},
  year={2008},
  publisher={Citeseer}
}

@article{berut2012experimental,
  title={Experimental verification of Landauer/'s principle linking information and thermodynamics},
  author={B{\'e}rut, A. and Arakelyan, A. and Petrosyan, A. and Ciliberto, S. and Dillenschneider, R. and Lutz, E.},
  journal={Nature},
  volume={483},
  number={7388},
  pages={187--189},
  year={2012},
  publisher={Nature Publishing Group}
}

@book{sen2006argumentative,
  title={{The argumentative Indian: Writings on Indian history, culture and identity}},
  author={Sen, A.},
  year={2006},
  publisher={Picador}
}

@book{boole1854investigation,
  title={An investigation of the laws of thought: on which are founded the mathematical theories of logic and probabilities},
  author={Boole, G.},
  volume={2},
  year={1854},
  publisher={Walton and Maberly}
}

@misc{math/9802029,
Author = {John C. Baez and James Dolan},
Title = {Categorification},
Year = {1998},
Howpublished = {In Higher Category Theory, Contemp. Math. 230, 1998, pp. 1-36.},
}

@misc{q-alg/9607028,
Author = {Louis Crane and David N. Yetter},
Title = {Examples of categorification},
Year = {1996},
Eprint = {arXiv:q-alg/9607028},
}

@inproceedings{Ghica:2007:GSS:1190216.1190269,
 author = {Ghica, Dan R.},
 title = {Geometry of synthesis: a structured approach to {VLSI} design},
 booktitle = {POPL},
 year = {2007},
 location = {Nice, France},
 pages = {363--375},
 numpages = {13},
 publisher = {ACM},
 keywords = {game semantics, geometry of interaction, syntactic control of interference, synthesis},
}

@incollection{selinger-graphical,
   author = {Selinger, P.},
   affiliation = {Department of Mathematics and Statistics, Dalhousie University, Halifax, NS Canada},
   title = {A Survey of Graphical Languages for Monoidal Categories},
   booktitle = {New Structures for Physics},
   series = {Lecture Notes in Physics},
   editor = {Coecke, Bob},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {},
   pages = {289-355},
   volume = {813},
   year = {2011}
}

@MISC{abramsky-2008,
  author = {Samson Abramsky and Bob Coecke},
  title = {Categorical quantum mechanics},
  note = {\url{arXiv:0808.1023} [quant-ph]},
  year = {2008}
}

@article{Selinger:2001:CCD:966910.966911,
 author = {Selinger, Peter},
 title = {Control categories and duality: on the categorical semantics of the lambda-mu calculus},
 journal = {Mathematical. Structures in Comp. Sci.},
 volume = {11},
 issue = {2},
 month = {April},
 year = {2001},
 pages = {207--260},
 numpages = {54},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@inproceedings{DBLP:conf/rta/Wadler05,
  author    = {Philip Wadler},
  title     = {Call-by-Value Is Dual to Call-by-Name - Reloaded},
  booktitle = {RTA},
  year      = {2005},
  pages     = {185-203},
  crossref  = {DBLP:conf/rta/2005},
}

@inproceedings{rc2011,
 author = {Bowman, William J. and James, Roshan P. and Sabry, Amr},
 title = {{Dagger Traced Symmetric Monoidal Categories and Reversible Programming}},
  booktitle = {RC},
  year      = {2011},
}

@InProceedings{rc2012,
  author =       {Roshan P. James and Amr Sabry},
  title =        {Isomorphic Interpreters from Logically Reversible Abstract Machines},
  booktitle = {RC},
  year      = {2012},
}

@inproceedings{DBLP:conf/popl/Wadler92,
  author    = {Philip Wadler},
  title     = {The Essence of Functional Programming},
  booktitle = {POPL},
  year      = {1992},
  pages     = {1-14},
  ee        = {http://doi.acm.org/10.1145/143165.143169},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{baez2011physics,
  title={Physics, topology, logic and computation: a Rosetta Stone},
  author={Baez, J. and Stay, M.},
  journal={New Structures for Physics},
  pages={95--172},
  year={2011},
  publisher={Springer}
}



@article{weinstein1996groupoids,
  title={Groupoids: unifying internal and external symmetry},
  author={Weinstein, A.},
  journal={Notices of the AMS},
  volume={43},
  number={7},
  pages={744--752},
  year={1996}
}

@book{higgins1971notes,
  title={Notes on categories and groupoids},
  author={Higgins, P.J.},
  volume={32},
  year={1971},
  publisher={Van Nostrand Reinhold}
}

@string{popl = {Proceedings of the {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages}}

@book{bloom1993iteration,
  title={Iteration theories: the equational logic of iterative processes},
  author={Bloom, S.L. and {\'E}sik, Z.},
  year={1993},
  publisher={Springer-Verlag}
}

@Book{nla.cat-vn1051288,
author = {Saunders {Mac Lane}},
title = {Categories for the working mathematician },
publisher = {Springer-Verlag},
year = {1971},
subjects = {Categories (Mathematics)}
}

@proceedings{DBLP:conf/ctcs/1985,
  editor    = {David H. Pitt and
               Samson Abramsky and
               Axel Poign{\'e} and
               David E. Rydeheard},
  title     = {Category Theory and Computer Programming, Tutorial and Workshop,
               Guildford, UK, September 16-20, 1985 Proceedings},
  booktitle = {CTCS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  year      = {1986},
}

@book{Halmos,
  author = {Halmos, Paul},
   note = {Reprinted by Springer-Verlag, Undergraduate Texts in Mathematics, 1974},
  publisher = {Van Nostrand},
  title = {Naive Set Theory},
  year = 1960
}

@article{Sabry:1997:RC:267959.269968,
 author = {Sabry, Amr and Wadler, Philip},
 title = {A reflection on call-by-value},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {19},
 number = {6},
 year = {1997},
 pages = {916--941},
 publisher = {ACM}
}

@inproceedings{Yokoyama:2007:RPL:1244381.1244404,
 author = {Yokoyama, Tetsuo and Gl\"{u}ck, Robert},
 title = {A reversible programming language and its invertible self-interpreter},
 booktitle = {PEPM},
 year = {2007},
 location = {Nice, France},
 pages = {144--153},
 numpages = {10},
 publisher = {ACM},
 keywords = {Janus, non-standard interpreter hierarchy, program inversion, reversible computing, reversible programming language, self-interpreter},
}

@inproceedings{Mellies:2006:FBS:2111603.2111605,
 author = {Melli\`{e}s, Paul-Andr{\'e}},
 title = {Functorial boxes in string diagrams},
 booktitle = {Proceedings of the 20th international conference on Computer Science Logic},
 series = {CSL'06},
 year = {2006},
 publisher = {Springer-Verlag},
}

@inproceedings{penrose-string-diagrams,
 author = {Penrose, R},
 title = {Applications of negative dimensional tensors},
 booktitle = {Combinatorial Mathematics and its Applications},
 year = {1971},
 publisher = {Academic Press}
}

@inproceedings{Axelsen:2011:RPC:1987171.1987176,
 author = {Axelsen, Holger Bock and Gl\"{u}ck, Robert},
 title = {What do reversible programs compute?},
 booktitle = {FOSSACS/ETAPS},
 year = {2011},
 pages = {42--56},
 numpages = {15},
 publisher = {Springer-Verlag},
}

@inproceedings{Danvy:2008:RRN:1813347.1813350,
 author = {Danvy, Olivier},
 title = {From reduction-based to reduction-free normalization},
 booktitle = {AFP},
 year = {2009},
 location = {Heijen, The Netherlands},
 pages = {66--164},
 numpages = {99},
 publisher = {Springer-Verlag},
}

@inproceedings{James:2012:IE:2103656.2103667,
 author = {James, Roshan P. and Sabry, Amr},
 title = {Information effects},
 booktitle = {POPL},
 year = {2012},
 location = {Philadelphia, PA, USA},
 pages = {73--84},
 numpages = {12},
 publisher = {ACM},
}

@TechReport{phantom,
  author =       {James Cheney and Ralf Hinze},
  title =        {First-Class Phantom Types},
  institution =  {Cornell Univ.},
  year =         2003}

@inproceedings{Xi:2003:GRD:604131.604150,
 author = {Xi, Hongwei and Chen, Chiyan and Chen, Gang},
 title = {Guarded recursive datatype constructors},
 booktitle = {POPL},
 year = {2003},
 location = {New Orleans, Louisiana, USA},
 pages = {224--235},
 numpages = {12},
 publisher = {ACM},
 keywords = {guarded recursive datatype constructors},
}

@inproceedings{Rendel:2010:ISD:1863523.1863525,
 author = {Rendel, Tillmann and Ostermann, Klaus},
 title = {Invertible syntax descriptions: unifying parsing and pretty printing},
 booktitle = {Symposium on Haskell},
 year = {2010},
 location = {Baltimore, Maryland, USA},
 pages = {1--12},
 numpages = {12},
 publisher = {ACM},
 keywords = {embedded domain specific languages, invertible computation, parser combinators, pretty printing},
}

@article{DBLP:journals/logcom/PierroHW05,
  author    = {Alessandra Di Pierro and
               Chris Hankin and
               Herbert Wiklicky},
  title     = {Probabilistic Lambda-calculus and Quantitative Program
               Analysis},
  journal   = {J. Log. Comput.},
  volume    = {15},
  number    = {2},
  year      = {2005},
}


@article{DBLP:journals/tcs/Barr95,
  author    = {Michael Barr},
  title     = {Nonsymmetric *-Autonomous Categories},
  journal   = {Theor. Comput. Sci.},
  volume    = {139},
  number    = {1{\&}2},
  year      = {1995},
  pages     = {115-130},
  ee        = {http://dx.doi.org/10.1016/0304-3975(94)00089-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/mscs/Barr91,
  author    = {Michael Barr},
  title     = {*-Autonomous Categories and Linear Logic},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {1},
  number    = {2},
  year      = {1991},
  pages     = {159-178},
  ee        = {http://dx.doi.org/10.1017/S0960129500001274},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{DBLP:books/daglib/0080381,
  author    = {Michael Barr and
               Charles Wells},
  title     = {Category theory for computing science (2. ed.)},
  publisher = {Prentice Hall},
  series    = {Prentice Hall international series in computer science},
  year      = {1995},
  isbn      = {978-0-13-323809-9},
  pages     = {I-XVII, 1-325},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{hammond1998data,
  title={Data speculation support for a chip multiprocessor},
  author={Hammond, L. and Willey, M. and Olukotun, K.},
  year={1998},
  publisher={ACM}
}

@inproceedings{DBLP:conf/popl/Mackie95,
  author    = {Ian Mackie},
  title     = {The Geometry of Interaction Machine},
  booktitle = {POPL},
  year      = {1995},
  pages     = {198-208},
  ee        = {http://doi.acm.org/10.1145/199448.199483},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Mackie2011,
  author    = {Ian Mackie},
  title     = {Reversible Higher-order Computations},
  booktitle = {Workshop on Reversible Computation},
  year      = {2011},
}

@inproceedings{girard1989towards,
  title={Towards a geometry of interaction},
  author={Girard, J.Y.},
  booktitle={Categories in computer science and logic: proceedings of
                  the AMS-IMS-SIAM Joint Summer Research Conference},
  volume={92},
  pages={69},
  year={1989},
  organization={Amer. Math. Society}
}

@article{girard1989geometry,
  title={Geometry of interaction 1: Interpretation of System F},
  author={Girard, J.Y.},
  journal={Studies in Logic and the Foundations of Mathematics},
  volume={127},
  pages={221--260},
  year={1989},
  publisher={Elsevier}
}

@article{Hasegawa:2009:TMC:1552068.1552069,
 author = {Hasegawa, Masahito},
 title = {On traced monoidal closed categories},
 journal = {MSCS},
 volume = {19},
 issue = {2},
 month = {April},
 year = {2009},
 issn = {0960-1295},
 pages = {217--244},
 numpages = {28},
 doi = {10.1017/S0960129508007184},
 acmid = {1552069},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}


@inproceedings{Hasegawa:1997:RCS:645893.671607,
 author = {Hasegawa, Masahito},
 title = {Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi},
 booktitle = {TLCA},
 year = {1997},
 pages = {196--213}
}

@article{mazur2008one,
  title={When is one thing equal to some other thing?},
  author={Mazur, B.},
  journal={Proof and Other Dilemmas: Mathematics and Philosophy, Mathematical Association of America, Washington, DC},
  pages={221--241},
  year={2008},
  publisher={Citeseer}
}

@inproceedings{DBLP:conf/calco/Abramsky05,
  author    = {Samson Abramsky},
  title     = {Abstract Scalars, Loops, and Free Traced and Strongly Compact
               Closed Categories},
  booktitle = {CALCO},
  year      = {2005},
}

@conference{joyal1996traced,
  title={{Traced monoidal categories}},
  author={Joyal, A. and Street, R. and Verity, D.},
  booktitle={Mathematical Proceedings of the Cambridge Philosophical Society},
  year={1996},
  organization={Cambridge Univ Press}
}

@phdthesis{Frank:1999:REC:930275,
 author = {Frank, Michael P.},
 title = {Reversibility for efficient computing},
 year = {1999},
 school = {Massachusetts Institute of Technology},
}

@inproceedings{DBLP:conf/icfp/ReedP10,
  author    = {Jason Reed and
               Benjamin C. Pierce},
  title     = {Distance makes the types grow stronger: a calculus for differential
               privacy},
  booktitle = {ICFP},
  year      = {2010},
}

@Article{PhysRevA.32.3266,
  title = {Reversible logic and quantum computers},
  author = {Peres, Asher },
  journal = {Phys. Rev. A},
  volume = {32},
  number = {6},
  year = {1985},
  month = {Dec},
  publisher = {American Physical Society}
}


@article{Shannon1948,
  author = {Claude Elwood Shannon},
  interhash = {754130207906fcec16a53d330eeff348},
  intrahash = {a1481c8475c34522e7f46a8dac9890a0},
  journal = {Bell Systems Technical Journal},
  pages = {379-423,623-656},
  title = {A mathematical theory of communication},
  volume = 27,
  year = 1948,
  timestamp = {2009.02.13},
  keywords = {imported},
  added-at = {2010-11-08T15:06:07.000+0100},
  file = {:A mathematical theory of communication.pdf:PDF},
  owner = {Yifan Peng},
  biburl = {http://www.bibsonomy.org/bibtex/2a1481c8475c34522e7f46a8dac9890a0/yfpeng}
}


@InProceedings{bio,
  author = {Luca Cardelli and Gianluigi Zavattaro},
  title = {On the Computational Power of Biochemistry},
  booktitle = {Third International Conference on Algebraic Biology},
  year = 2008
}

@INPROCEEDINGS{Massey,
    author = {James L. Massey},
    title = {Guessing and Entropy},
    booktitle = {Proceedings of the IEEE International Symposium on Information Theory},
    year = {1994},
    pages = {204}
}

@inproceedings{Prabhu:2010:SPS:1806596.1806603,
 author = {Prabhu, Prakash and Ramalingam, Ganesan and Vaswani, Kapil},
 title = {Safe programmable speculative parallelism},
 booktitle = {ACM Conference on Programming Language Design and Implementation},
 year = {2010},
 location = {Toronto, Ontario, Canada},
 pages = {50--61},
 numpages = {12},
 publisher = {ACM},
 keywords = {purity, rollback freedom, safety, speculative parallelism, value speculation},
}


@inproceedings{Macii:1996:ECE:874066.875828,
 author = {Macii, Enrico and Poncino, Massimo},
 title = {Exact Computation of the Entropy of a Logic Circuit},
 booktitle = {Proceedings of the 6th Great Lakes Symposium on VLSI},
 year = {1996},
 acmid = {875828},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
}

@article{ClarkHM07,
 author = {Clark, David and Hunt, Sebastian and Malacaria, Pasquale},
 title = {A static analysis for quantifying information flow in a simple imperative language},
 journal = {J. Comput. Secur.},
 volume = {15},
 issue = {3},
 month = {August},
 year = {2007},
 pages = {321--371},
 numpages = {51},
 publisher = {IOS Press},
 keywords = {Security, confidentiality, information flow, information theory, leakage, measurement, program analysis, quantify interference, static analysis, while language},
}

@inproceedings{malacaria2007assessing,
 author = {Malacaria, Pasquale},
 title = {Assessing security threats of looping constructs},
 booktitle = {POPL},
 year = {2007},
 location = {Nice, France},
 pages = {225--235},
 numpages = {11},
 publisher = {ACM},
 keywords = {information theory, language semantics, security},
}

@article{DiPierro:2006:RCL:1166042.1166047,
 author = {Di Pierro, Alessandra and Hankin, Chris and Wiklicky, Herbert},
 title = {Reversible combinatory logic},
 journal = {MSCS},
 volume = {16},
 issue = {4},
 month = {August},
 year = {2006},
 pages = {621--637},
 numpages = {17},
 acmid = {1166047},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@inproceedings{Kluge:1999:SEMCD,
 author = {Kluge, Werner E.},
 title = {A Reversible {SE(M)CD} Machine},
 booktitle = {International Workshop on Implementation of Functional Languages},
 year = {2000},
 pages = {95--113},
 numpages = {19},
 publisher = {Springer-Verlag},
}

@inproceedings{Stoddart2006,
  author    = {Bill Stoddart and
               Frank Zeyda and
               Robert Lynas},
  title     = {A Design-Based Model of Reversible Computation},
  booktitle = {UTP},
  year      = {2006},
  pages     = {63-83},
  ee        = {http://dx.doi.org/10.1007/11768173_4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@Comment crossref  = {DBLP:conf/utp/2006},


@article{danos2004reversible,
  title={{Reversible communicating systems}},
  author={Danos, V. and Krivine, J.},
  journal={Concurrency Theory},
  pages={292--307},
  year={2004},
  publisher={Springer}
}

@inproceedings{sabelfeld2005dimensions,
 author = {Sabelfeld, Andrei and Sands, David},
 title = {Dimensions and Principles of Declassification},
 booktitle = {Proceedings of the 18th IEEE workshop on Computer Security Foundations},
 year = {2005},
 isbn = {0-7695-2340-4},
 pages = {255--269},
 numpages = {15},
 url = {http://portal.acm.org/citation.cfm?id=1068506.1068880},
 doi = {10.1109/CSFW.2005.15},
 acmid = {1068880},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
}


@conference{chong2008end,
  title={{End-to-end enforcement of erasure and declassification}},
  author={Chong, S. and Myers, A.C.},
  booktitle={Computer Security Foundations Symposium. CSF},
  pages={98--111},
  year={2008},
  organization={IEEE}
}

@article{askarov2008termination,
  title={{Termination-insensitive noninterference leaks more than just a bit}},
  author={Askarov, A. and Hunt, S. and Sabelfeld, A. and Sands, D.},
  journal={Computer Security-ESORICS 2008},
  pages={333--348},
  year={2008},
  publisher={Springer}
}

@article{denning1976lattice,
 author = {Denning, Dorothy E.},
 title = {A lattice model of secure information flow},
 journal = {Commun. ACM},
 volume = {19},
 issue = {5},
 month = {May},
 year = {1976},
 pages = {236--243},
 numpages = {8},
 publisher = {ACM},
 keywords = {information flow, lattice, program certification, protection, security, security class},
}

@article{bennett2010notes,
  title={{Notes on the history of reversible computation}},
  author={Bennett, C.H.},
  journal={IBM Journal of Research and Development},
  volume={32},
  number={1},
  pages={16--23},
  year={2010},
  publisher={IBM}
}

@article{Baker:1992:LLL,
 author = {Baker, Henry G.},
 title = {Lively linear {Lisp}: --- look ma, no garbage! ---},
 journal = {SIGPLAN Not.},
 volume = {27},
 issue = {8},
 month = {August},
 year = {1992},
 pages = {89--98},
 numpages = {10},
 publisher = {ACM},
}

@inproceedings{Baker:1992:NFT,
 author = {Baker, Henry G.},
 title = {NREVERSAL of Fortune - The Thermodynamics of Garbage Collection},
 booktitle = {Proceedings of the International Workshop on Memory Management},
 year = {1992},
 pages = {507--524},
 numpages = {18},
 publisher = {Springer-Verlag},
}


@article{Baker:1994:LLP,
 author = {Baker, Henry G.},
 title = {Linear logic and permutation stacks - the Forth shall be first},
 journal = {SIGARCH Comput. Archit. News},
 volume = {22},
 issue = {1},
 month = {March},
 year = {1994},
 pages = {34--43},
 numpages = {10},
 publisher = {ACM},
}

@inproceedings{Yokoyama:2008:PRP,
 author = {Yokoyama, Tetsuo and Axelsen, Holger Bock and Gl\"{u}ck, Robert},
 title = {Principles of a reversible programming language},
 booktitle = {Conference on Computing Frontiers},
 year = {2008},
 location = {Ischia, Italy},
 pages = {43--54},
 numpages = {12},
 publisher = {ACM},
 keywords = {backward determinism, fast fourier transform, inverse semantics, reversible computing, turing completeness},
}

@conference{abadi2002faithful,
  title={{Faithful ideal models for recursive polymorphic types}},
  author={Abadi, M. and Pierce, B. and Plotkin, G.},
  booktitle={Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on},
  pages={216--225},
  isbn={0818619546},
  year={2002},
  organization={IEEE}
}

@conference{macqueen1984ideal,
  title={{An ideal model for recursive polymorphic types}},
  author={MacQueen, D. and Plotkin, G. and Sethi, R.},
  booktitle={Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages},
  pages={165--174},
  isbn={0897911253},
  year={1984},
  organization={ACM}
}

@Comment Can't find this paper on ACM
@inproceedings{Mu:2001:FQP,
  author    = {Shin-Cheng Mu and
               Richard S. Bird},
  title     = {Functional Quantum Programming},
  booktitle = {APLAS},
  year      = {2001},
  pages     = {75-88},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
  @Comment crossref  = {DBLP:conf/aplas/2001},

@Comment This is not there on ACM
@inproceedings{Mu:2004:ILRC,
  author    = {Shin-Cheng Mu and
               Zhenjiang Hu and
               Masato Takeichi},
  title     = {An Injective Language for Reversible Computation},
  booktitle = {MPC},
  year      = {2004},
  pages     = {289-313},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
  @Comment crossref  = {DBLP:conf/mpc/2004},


@article{Green:2008:RIC,
 author = {Green, Alexander S. and Altenkirch, Thorsten},
 title = {From Reversible to Irreversible Computations},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {210},
 month = {July},
 year = {2008},
 pages = {65--74},
 numpages = {10},
 publisher = {Elsevier Science Publishers B. V.},
 keywords = {Reversible computation, categorical models, irreversible computation, quantum computation},
}

@article{Zuliani:2001:LR,
 author = {Zuliani, P.},
 title = {Logical reversibility},
 journal = {IBM J. Res. Dev.},
 volume = {45},
 issue = {6},
 month = {November},
 year = {2001},
 pages = {807--818},
 numpages = {12},
 publisher = {IBM Corp.},
}

@InProceedings{stoddart2003forth,
  title={{Using Forth in an Investigation into Reversible Computation}},
  author={Stoddart, B.},
  booktitle = {EuroForth},
  pages={1-8},
  year={2003}
}

@article{bennett2003notes,
  title={{Notes on Landauer's principle, reversible computation, and Maxwell's Demon}},
  author={Bennett, C.H.},
  journal={Studies In History and Philosophy of Science Part B: Studies In History and Philosophy of Modern Physics},
  volume={34},
  number={3},
  pages={501--510},
  year={2003},
  publisher={Elsevier}
}

@article{fredkin1982conservative,
  title={{Conservative logic}},
  author={Fredkin, E. and Toffoli, T.},
  journal={International Journal of Theoretical Physics},
  volume={21},
  number={3},
  pages={219--253},
  year={1982},
  publisher={Springer}
}

@article{10.1109/LICS.2010.23,
author = {Noam Zeilberger},
title = {Polarity and the Logic of Delimited Continuations},
journal = {LICS},
year = {2010}
}

@article{Bennett:1973:LRC,
 author = {Bennett, C. H.},
 title = {Logical reversibility of computation},
 journal = {IBM J. Res. Dev.},
 volume = {17},
 issue = {6},
 month = {November},
 year = {1973},
 pages = {525--532},
 numpages = {8},
 publisher = {IBM Corp.},
}

@conference{wadler1990linear,
  title={{Linear types can change the world}},
  author={Wadler, P.},
  booktitle={IFIP TC},
  volume={2},
  pages={347--359},
  year={1990},
  organization={Citeseer}
}

@InProceedings{1079699,
    author =     {Thorsten Altenkirch and Jonathan Grattage},
    title =      {A Functional Quantum Programming Language},
    booktitle =  {LICS},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June},
    pages =      {249--258},
    location =   {Chicago, USA},
    publisher =	 {IEEE Computer Society Press}
  }

@article{altenkirch2005qml,
  title={{QML: Quantum data and control}},
  author={Altenkirch, T. and Grattage, J.},
  year={2005},
}

@article{springerlink:10.1007/BF02650179,
   author = {Feynman, Richard},
   title = {Simulating physics with computers},
   journal = {International Journal of Theoretical Physics},
   pages = {467-488},
   volume = {21},
   issue = {6},
   year = {1982}
}

@Article{rauszer,
  author =       {C. Rauszer},
  title =        {Semi-boolean algebras and their applications to intuitionistic logic with dual operators},
  journal =      {Fundamenta Mathematicae},
  year =         1974,
  volume =    83,
  pages =     {219-249}
}

@InCollection{rauszer2,
  author =       {C. Rauszer},
  title =        {An algebraic and {Kripke}-style approach to a certain
                  extension  of intuitionistic logic},
  booktitle =    {Dissertationes Mathmaticae},
  publisher = {Institut Math\'ematique de l'Acad\'emie Polonaise des Sciences},
  year =      1980,
  volume =    167
}

@article{Crolard01082004,
author = {Crolard, Tristan},
title = {A Formulae-as-Types Interpretation of Subtractive Logic},
volume = {14},
number = {4},
pages = {529-570},
year = {2004},
journal = {Journal of Logic and Computation}
}

@phdthesis{grattage2006thesis,
  title={{QML: A functional quantum programming language}},
  author={Grattage, J.},
  year={2006},
  school={The University of Nottingham}
}

@misc{finiteQC,
  title={{Quantum Computing over Finite Fields}},
  author={Roshan P. James and Gerardo Ortiz and Amr Sabry},
  year={2011},
  howpublished = {\url{http://arxiv.org/abs/1101.3764}},
}

@article{Matos:2003:LPS,
 author = {Matos, Armando B.},
 title = {Linear programs in a simple reversible language},
 journal = {Theor. Comput. Sci.},
 volume = {290},
 issue = {3},
 month = {January},
 year = {2003},
 pages = {2063--2074},
 numpages = {12},
 publisher = {Elsevier Science Publishers Ltd.},
 keywords = {group of modular matrices, loop languages, reversibility},
}


@article{Gluck:2005,
 author = {Gl\"{u}ck, Robert and Kawabe, Masahiko},
 title = {Revisiting an automatic program inverter for {Lisp}},
 journal = {SIGPLAN Not.},
 volume = {40},
 issue = {5},
 month = {May},
 year = {2005},
 pages = {8--17},
 numpages = {10},
 publisher = {ACM},
}

@book{Church51,
 author = {A. Church},
 title = {{The Calculi of Lambda-Conversion}},
 series = {Annals of Mathematical Studies},
 volume = {6},
 note   = {(second printing, first appeared 1941)},
 publisher = {Princeton University Press},
 address = {Princeton},
 year = 1951,
 topics = {FP - Lambda Calculi}
}

@article{Landauer:1961,
 author = {Landauer, R.},
 title = {Irreversibility and heat generation in the computing process},
 journal = {IBM J. Res. Dev.},
 volume = {5},
 issue = {3},
 month = {July},
 year = {1961},
 pages = {183--191},
 numpages = {9},
 publisher = {IBM Corp.},
}

@article{zdancewic2002linear,
 author = {Zdancewic, Steve and Myers, Andrew C.},
 title = {Secure Information Flow via Linear Continuations},
 journal = {Higher Order Symbol. Comput.},
 volume = {15},
 number = {2-3},
 year = {2002},
 pages = {209--234},
 publisher = {Kluwer Academic Publishers},
}


@article{Volpano1996,
  author    = {Dennis M. Volpano and
               Cynthia E. Irvine and
               Geoffrey Smith},
  title     = {A Sound Type System for Secure Flow Analysis},
  journal   = {Journal of Computer Security},
  volume    = {4},
  number    = {2/3},
  year      = {1996},
  pages     = {167-188},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{myerssab,
  title = {Language-based information-flow security},
  author = {Andrei Sabelfeld and Andrew Myers},
  journal = {IEEE Journal on Selected Areas in Communications},
  volume = 21,
  number = 1,
  pages = {5-19},
  year = 2003
}


@article{felleisen1987syntactic,
  title={{A syntactic theory of sequential control* 1}},
  author={Felleisen, M. and Friedman, D.P. and Kohlbecker, E. and Duba, B.},
  journal={Theoretical computer science},
  volume={52},
  number={3},
  pages={205--237},
  year={1987},
  publisher={Elsevier}
}

@article{1324180,
 author = {Ma, Xiaojun and Huang, Jing and Lombardi, Fabrizio},
 title = {A model for computing and energy dissipation of molecular {QCA} devices and circuits},
 journal = {J. Emerg. Technol. Comput. Syst.},
 volume = {3},
 number = {4},
 year = {2008},
 pages = {1--30},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{605411,
 author = {Zeng, Heng and Ellis, Carla S. and Lebeck, Alvin R. and Vahdat, Amin},
 title = {ECOSystem: managing energy as a first class operating system resource},
 journal = {SIGPLAN Not.},
 volume = {37},
 number = {10},
 year = {2002},
 pages = {123--132},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{1068880,
 author = {Sabelfeld, Andrei and Sands, David},
 title = {Dimensions and Principles of Declassification},
 booktitle = {CSFW '05: Proceedings of the 18th IEEE workshop on Computer Security Foundations},
 year = {2005},
 isbn = {0-7695-2340-4},
 pages = {255--269},
 doi = {http://dx.doi.org/10.1109/CSFW.2005.15},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

@book{mitchell1996foundations,
  title={{Foundations for programming languages}},
  author={Mitchell, J.C.},
  year={1996},
  publisher={MIT press Cambridge, MA}
}

@article{mcbride2007applicative,
  title={{Applicative programming with effects}},
  author={McBride, C. and Paterson, R.},
  journal={Journal of functional programming},
  volume={18},
  number={01},
  pages={1--13},
  year={2007},
  publisher={Cambridge Univ Press}
}

@BOOK{PIERCE91,
  author = {Benjamin C. Pierce},
  title = {Basic Category Theory for Computer Scientists},
  year = {1991},
  publisher = {MIT Press},
  fullisbn = {0-262-66071-7},
  orderinginfo = {MIT PRESS 55 Hayward ST. Cambridge Mass 02142 USA
                  800-356-0343},
  europeinfo = {14 Bloomsbury Square London WC1A 2LP U.K. Facsimile:
                  071-404-0601},
  plclub = {Yes},
  bcp = {Yes},
  keys = {books}
}

@book{lawvere1997conceptual,
  title={Conceptual mathematics: a first introduction to categories},
  author={Lawvere, F.W. and Schanuel, S.H.},
  year={1997},
  publisher={Cambridge University Press}
}

@article{moggi1991notions,
  title={Notions of computation and monads},
  author={Moggi, E.},
  journal={Information and computation},
  volume={93},
  number={1},
  pages={55--92},
  year={1991},
  publisher={Elsevier}
}

@BOOK{Pierce:TypeSystems,
  author = {Benjamin C. Pierce},
  title = {Types and Programming Languages},
  publisher = {MIT Press},
  year = 2002,
  plclub = {Yes},
  bcp = {Yes},
  keys = {books},
  homepage = {http://www.cis.upenn.edu/~bcpierce/tapl},
  errata = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
}
@BOOK{ATTAPL,
  editor = {Benjamin C. Pierce},
  title = {Advanced Topics in Types and Programming Languages},
  publisher = {MIT Press},
  year = 2005,
  plclub = {Yes},
  bcp = {Yes},
  keys = {books},
  homepage = {http://www.cis.upenn.edu/~bcpierce/attapl}
}

@book{gunter1992semantics,
  title={{Semantics of programming languages: structures and techniques}},
  author={Gunter, C.A.},
  year={1992},
  publisher={The MIT Press}
}

@article{kennedy2006securing,
  title={{Securing the. NET programming model}},
  author={Kennedy, A.},
  journal={Theoretical Computer Science},
  volume={364},
  number={3},
  pages={311--317},
  year={2006},
  publisher={Elsevier}
}

@inproceedings{ahmed2008typed,
 author = {Ahmed, Amal and Blume, Matthias},
 title = {Typed closure conversion preserves observational equivalence},
 booktitle = {ICFP},
 year = {2008},
 location = {Victoria, BC, Canada},
 pages = {157--168},
 numpages = {12},
 publisher = {ACM},
 keywords = {equivalence-preserving compilation, full abstraction, step-indexed logical relations, typed closure conversion},
}

@article{abramsky2005structural,
 author = {Abramsky, Samson},
 title = {A structural approach to reversible computation},
 journal = {Theor. Comput. Sci.},
 volume = {347},
 issue = {3},
 month = {December},
 year = {2005},
 pages = {441--464},
 numpages = {24},
 acmid = {1131863},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
 keywords = {automata, geometry of interaction, linear combinatory algebra, reversible computation, term-rewriting},
}

@conference{abramsky1994full,
  title={{Full Abstraction for PCF (extended abstract)}},
  author={Abramsky, S. and Malacaria, P. and Jagadeesan, R.},
  booktitle={Theoretical Aspects of Computer Software},
  pages={1--15},
  year={1994},
  organization={Springer}
}

@article{launchbury1995state,
  title={{State in haskell}},
  author={Launchbury, J. and Peyton Jones, S.L.},
  journal={Lisp and Symbolic Computation},
  volume={8},
  number={4},
  pages={293--341},
  year={1995},
  publisher={Springer}
}

@article{felleisen1992revised,
  title={{The revised report on the syntactic theories of sequential control and state}},
  author={Felleisen, M. and Hieb, R.},
  journal={TCS},
  volume={103},
  number={2},
  pages={235--271},
  year={1992},
  publisher={Citeseer}
}

@conference{swarup1991assignments,
  title={{Assignments for applicative languages}},
  author={Swarup, V. and Reddy, U. and Ireland, E.},
  booktitle={Functional Programming Languages and Computer Architecture},
  pages={192--214},
  year={1991},
  organization={Springer}
}

@conference{cartwright1992observable,
  title={{Observable sequentiality and full abstraction}},
  author={Cartwright, R. and Felleisen, M.},
  booktitle={Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={328--342},
  year={1992},
  organization={ACM}
}

@article{Ahmed:2011:ECT:2034574.2034830,
 author = {Ahmed, Amal and Blume, Matthias},
 title = {An equivalence-preserving CPS translation via multi-language semantics},
 journal = {SIGPLAN Not.},
 issue_date = {September 2011},
 year = {2011},
 pages = {431--444},
 publisher = {ACM},
 address = {New York, NY, USA}
}

@inproceedings{Necula:1997:PC:263699.263712,
 author = {Necula, George C.},
 title = {Proof-carrying code},
 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '97},
 year = {1997},
 pages = {106--119},
 publisher = {ACM},
}



@article{lutz1982janus,
  title={Janus: a time-reversible language},
  author={Lutz, C. and Derby, H.},
  journal={Unpublished report, Ph. D. Dissertation, California Institute of Technology},
  year={1982}
}

@inproceedings{bershad1995protection,
  title={Protection is a software issue},
  author={Bershad, B.N. and Savage, S. and Pardyak, P. and Becker, D. and Fiuczynski, M. and Sirer, E.G.},
  booktitle={Hot Topics in Operating Systems, 1995.(HotOS-V), Proceedings., Fifth Workshop on},
  pages={62--65},
  year={1995},
  organization={IEEE}
}

@article{krivine2012verification,
  title={A verification technique for reversible process algebra},
  author={Krivine, J.},
  journal={Reversible Computation, Lecture Notes in Computer Science},
  year={2012}
}

@article{phillipsreversible,
  title={A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway},
  author={Phillips, I. and Ulidowski, I. and Yuen, S.},
  journal={Reversible Computation, Lecture Notes in Computer Science},
  year={2012}
}

@inproceedings{Morita2001,
 title={A Simple Universal Logic Element and Cellular Automata for Reversible Computing},
 author={Morita, Kenichi},
 pages={102--113},
 year={2001},
 booktitle={Machines, Computations, and Universality},
 series={Lecture Notes in Computer Science},
 publisher={Springer Berlin Heidelberg}
}


@inproceedings{Morita:2007,
 author = {Morita, Kenichi and Yamaguchi, Yoshikazu},
 title = {A universal reversible turing machine},
 booktitle = {Proceedings of the 5th international conference on Machines, computations, and universality},
 series = {MCU07},
 year = {2007},
 pages = {90--98},
 publisher = {Springer-Verlag}
}

@article{lecerf1963machines,
  title={Machines de Turing r{\'e}versibles},
  author={Lecerf, Y.},
  journal={Comptes Rendus},
  pages={2597--2600},
  year={1963}
}

@TECHREPORT{Filinski96controllingeffects,
    author = {Andrzej Filinski and John Reynolds and Stephen Brookes},
    title = {Controlling Effects},
    institution = {School of Computer Science, Carnegie Mellon University},
    year = {1996}
}

@conference{plotkin2002notions,
  title={{Notions of computation determine monads}},
  author={Plotkin, G. and Power, J.},
  booktitle={Foundations of Software Science and Computation Structures},
  pages={373--393},
  year={2002},
  organization={Springer}
}

@article{plotkin2004computational,
  title={{Computational effects and operations: An overview}},
  author={Plotkin, G.D. and Power, J.},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={73},
  pages={149--163},
  year={2004},
  publisher={Citeseer}
}

@inproceedings{Curien:2000,
 author = {Curien, Pierre-Louis and Herbelin, Hugo},
 title = {The duality of computation},
 booktitle = {ICFP},
 year = {2000}
}

@inproceedings{Riecke:1991:FAT:99583.99617,
 author = {Riecke, Jon G.},
 title = {Fully abstract translations between functional languages},
 booktitle = {Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1991},
 isbn = {0-89791-419-8},
 location = {Orlando, Florida, United States},
 pages = {245--254},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/99583.99617},
 doi = {http://doi.acm.org/10.1145/99583.99617},
 acmid = {99617},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{plotkin1975calculus,
  author    = {Gordon D. Plotkin},
  title     = {Call-by-Name, Call-by-Value and the lambda-Calculus},
  journal   = {Theor. Comput. Sci.},
  volume    = {1},
  number    = {2},
  year      = {1975},
  pages     = {125-159},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Sabry:98,
  title={{What is a purely functional language?}},
  author={Sabry, A.},
  journal={Journal of Functional Programming},
  volume={8},
  number={01},
  pages={1--22},
  year={1998},
  publisher={Cambridge University Press}
}

@inproceedings{Alimarine:2005:BAA,
 author = {Alimarine, Artem and Smetsers, Sjaak and van Weelden, Arjen and van Eekelen, Marko and Plasmeijer, Rinus},
 title = {There and back again: arrows for invertible programming},
 booktitle = {ACM Workshop on Haskell},
 year = {2005},
 location = {Tallinn, Estonia},
 pages = {86--97},
 numpages = {12},
 publisher = {ACM},
 keywords = {arrows, haskell, invertible program construction, polytypic programming},
}

@inproceedings{Toffoli:1980,
 author = {Toffoli, Tommaso},
 title = {Reversible Computing},
 booktitle = {Proceedings of the 7th Colloquium on Automata, Languages and Programming},
 year = {1980},
 pages = {632--644},
 numpages = {13},
 publisher = {Springer-Verlag},
}



@article{Sestoft:90,
  title={{Referential transparency, definiteness and unfoldability}},
  author={S{\o}ndergaard, H. and Sestoft, P.},
  journal={Acta Informatica},
  volume={27},
  number={6},
  pages={505--517},
  year={1990},
  publisher={Springer}
}

@inproceedings{Wadler:2003,
 author = {Wadler, Philip},
 title = {Call-by-value is dual to call-by-name},
 booktitle = {ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming},
 year = {2003},
 isbn = {1-58113-756-7},
 pages = {189--201},
 location = {Uppsala, Sweden},
 doi = {http://doi.acm.org/10.1145/944705.944723},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{Hughes:2000,
 author = {Hughes, John},
 title = {Generalising monads to arrows},
 journal = {Sci. Comput. Program.},
 volume = {37},
 number = {1-3},
 year = {2000},
 pages = {67--111},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 }

@article{Lindley:2010,
  title={{The arrow calculus}},
  author={Lindley, S. and Wadler, P. and Yallop, J.},
  journal={Journal of Functional Programming},
  volume={20},
  number={01},
  pages={51--69},
  year={2010},
  publisher={Cambridge University Press}
}

@inproceedings{Paterson:2001,
 author = {Paterson, Ross},
 title = {A new notation for arrows},
 booktitle = {ICFP '01: Proceedings of the sixth ACM SIGPLAN international conference on Functional programming},
 year = {2001},
 isbn = {1-58113-415-0},
 pages = {229--240},
 location = {Florence, Italy},
 doi = {http://doi.acm.org/10.1145/507635.507664},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{Fiore:2004,
 author = {Fiore, Marcelo},
 title = {Isomorphisms of generic recursive polynomial types},
 booktitle = {POPL},
 year = {2004},
 location = {Venice, Italy},
 pages = {77--88},
 numpages = {12},
 publisher = {ACM},
 keywords = {Gr\"{o}bner bases, data structure, recursive types, rigs, semigroups, type isomorphism, type theory, word problem},
}

@conference{piee,
  title={{The Two Dualities of Computation : Negative and Fractional Types}},
  author={Roshan P. James and Amr Sabry},
  booktitle={submitted to ICFP},
  year={2012}
}

@inproceedings{findler,
   author = "Jacob Matthews and Robert Bruce Findler",
   title = "An Operational Semantics for {R{\textsuperscript 5}RS} {S}cheme",
   pages = "41--54",
   crossref = "scheme2005",
   url = "http://repository.readscheme.org/ftp/papers/sw2005/matthews.pdf"
}

@InProceedings{Fil:replm,
  author =       "Andrzej Filinski",
  title =        "Representing Layered Monads",
  booktitle =    popl,
  pages =        "175--188",
  year =         "1999",
  URL =          "http://www.brics.dk/~andrzej/papers/RLM.ps.gz",
  isbn = {1-58113-095-3},
  location = {San Antonio, Texas, United States},
  doi = {http://doi.acm.org/10.1145/292540.292557},
  publisher = acm
}


@article{leroy-exceptions,
 author = {Xavier Leroy and Fran{\c c}ois Pessaux},
 title = {Type-Based Analysis of Uncaught Exceptions},
 journal = j_toplas,
 volume = {22},
 number = {2},
 year = {2000},
 issn = {0164-0925},
 pages = {340--377},
 doi = {http://doi.acm.org/10.1145/349214.349230},
 publisher = {ACM Press},
 address = {New York, NY, USA}
 }

@InProceedings{	balat-memoization,
  author	= "Vincent Balat and Olivier Danvy",
  title		= "Memoization in Type-Directed Partial Evaluation",
  pages		= "78--92",
  crossref	= "gpce2002",
  url		= "http://www.brics.dk/RS/02/33/BRICS-RS-02-33.ps.gz http://www.brics.dk/RS/02/33/BRICS-RS-02-33.pdf"
}

@InProceedings{	balat-extensional,
  author	= "Vincent Balat and Di Cosmo, Roberto and Marcelo Fiore",
  title		= "Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums",
  pages		= "64--76",
  crossref	= "popl2004",
  url		= "http://www.cl.cam.ac.uk/~mpf23/papers/Types/tdpe.pdf"
}

@Article{	biernacka-operational-lmcs,
  author	= "Ma{\l}gorzata Biernacka and Dariusz Biernacki and Olivier Danvy",
  title		= "An Operational Foundation for Delimited Continuations in the {CPS} Hierarchy",
  journal	= j_lmcs,
  year		= 2005,
  volume	= 1,
  number	= "2:5",
  url		= "http://arxiv.org/abs/cs.LO/0508048"
}

@InProceedings{	biernacki-interpreter,
  author	= {Dariusz Biernacki and Olivier Danvy},
  title		= {From Interpreter to Logic Engine by Defunctionalization},
  pages		= {143--159},
  crossref	= {lopstr2003},
  url		= "http://www.brics.dk/RS/04/Abs/BRICS-RS-04-Abs/BRICS-RS-04-Abs.html#BRICS-RS-04-5"
}

@InProceedings{	danvy-type-directed,
  author	= "Olivier Danvy",
  title		= "Type-Directed Partial Evaluation",
  pages		= "242--257",
  crossref	= "popl1996",
  url		= "ftp://ftp.daimi.au.dk/pub/empl/danvy/Papers/danvy-popl96.ps.gz"
}

@InProceedings{	dybjer-normalization,
  author	= "Peter Dybjer and Andrzej Filinski",
  title		= "Normalization and Partial Evaluation",
  pages		= "137--192",
  crossref	= "appsem2000",
  url		= "http://www.cs.chalmers.se/~peterd/papers/Caminha.ps"
}

@inproceedings{FriedH85,
 author = {Daniel P. Friedman and Christopher T. Haynes},
 title = {Constraining Control},
 booktitle = popl,
 year = {1985},
 isbn = {0-89791-147-4},
 pages = {245--254},
 location = {New Orleans, Louisiana, United States},
 doi = {http://doi.acm.org/10.1145/318593.318654},
 publisher = {ACM Press}
 }

@inproceedings{LiangTransformers,
 author = {Sheng Liang and Paul Hudak and Mark Jones},
 title = {Monad transformers and modular interpreters},
 booktitle = popl,
 year = {1995},
 isbn = {0-89791-692-1},
 pages = {333--343},
 location = {San Francisco, California, United States},
 doi = {http://doi.acm.org/10.1145/199448.199528},
 publisher = acm
 }

@InProceedings{prepose,
    author="Oleg Kiselyov and Shan, Chung-chieh",
    title="Functional Pearl: Implicit Configurations---or, Type Classes Reflect the Values of Types",
    pages = "33--44",
    crossref="haskell2004"
}

@Proceedings{	haskell2004,
  title		= "Proceedings of the 2004 {H}askell Workshop",
  booktitle	= "Proceedings of the 2004 {H}askell Workshop",
  publisher	= acm,
  year		= 2004,
  location	= "Snowbird, UT"
}


@InProceedings{lewis-implicit,
  author	= "Jeffrey R. Lewis and Mark B. Shields and Erik Meijer and John Launchbury",
  title		= "Implicit Parameters: Dynamic Scoping with Static Types",
  pages		= "108--118",
  crossref	= "popl2000"
}

@Proceedings{	popl1996,
  key		= "{\relax POPL}",
  title		= popl,
  booktitle	= popl,
  publisher	= pub_acm,
  year		= 1996,
  isbn		= {0-89791-769-3},
  issn		= "0730-8566",
  location	= "St.~Petersburg Beach, FL"
}

@Proceedings{popl2000,
  key		= "{\relax POPL}",
  title		= popl,
  booktitle	= popl,
  publisher	= acm,
  year		= 2000,
  location	= "Boston"
}

@InProceedings{unwind,
  author =       {Dorai Sitaram},
  title =        {Unwind-Protect in Portable {S}cheme},
  crossref="scheme2003",
  pages="48--52"
}

@Proceedings{	scheme2003,
  editor	= "Matthew Flatt",
  title		= "Proceedings of the 4th Workshop on {S}cheme and Functional Programming",
  booktitle	= "Proceedings of the 4th Workshop on {S}cheme and Functional Programming",
  publisher	= "School of Computing, University of Utah",
  year		= 2003,
  month		= "7~"  # nov,
  number	= "UUCS-03-023",
  url		= "http://www.cs.utah.edu/techreports/2003/pdf/UUCS-03-023.pdf http://www.cs.utah.edu/techreports/2003/pdf/UUCS-03-023.ps.gz http://scheme2003.flux.utah.edu/",
  location	= "Boston"
}

@Article{R5RS,
  author =       "Richard Kelsey and William Clinger and
                  Jonathan {Rees, editors}",
  title =        "Revised${}^5$ Report on the Algorithmic Language {S}cheme",
  journal =      "Higher-Order and Symbolic Computation",
  year =         1998,
  volume =       11,
  number =       1,
  pages =        "7-105",
  note =         "Also appears in ACM SIGPLAN Notices 33(9), September 1998"
}

@Inproceedings{Mog+Fag:FOSSACS-2003,
  author =       {E. Moggi and S. Fagorzi},
  title =        {A Monadic Multi-stage Metalanguage},
  year =         2003,
  booktitle =    {{FoSSaCS} 2003},
  series =       LNCS,
  publisher =    SV
}

@TechReport{olegtr,
  author =       {Oleg Kiselyov},
  title =        {How to remove a dynamic prompt: static and dynamic delimited continuation operators are equally expressible},
  institution =  {Department of Computer Science, Indiana University},
  year =         2005,
  number =       {611}
}

@Misc{mcp,
  author =       {Stuart Russell},
  title =        {The Missionaries and Cannibals Domain},
  howpublished = {\url{http://www.cs.berkeley.edu/~russell/code/search/domains/cannibals.lisp}},
  year =         1997
}

@Misc{evil-nlab,
  author =       {{nLab}},
  title =        {Evil},
  howpublished = {\url{http://ncatlab.org/nlab/show/evil}},
  year =         {accessed on 19 April 2012}
}


@book{BookNaish,
 author = {Lee Naish},
 title = {Negation and control in Prolog??? Ref on his web site?},
 year = {1986},
 isbn = {0-387-16815-X},
 publisher = {Springer-Verlag New York, Inc.}
 }

@article {springerlink:10.1007/BF01211087,
   author = {Ross, Brian J.},
   affiliation = {Department of Computer Science Brock University L2S 3A1 St Catharines Ontario Canada},
   title = {Running programs backwards: The logical inversion of imperative computation},
   journal = {Formal Aspects of Computing},
   publisher = {Springer London},
   keyword = {Computer Science},
   pages = {331-348},
   volume = {9},
   issue = {3},
   year = {1997}
}

@article {springerlink:10.1007/BF02120864,
   author = {Rauszer, Cecylia},
   title = {A formalization of the propositional calculus of {H-B} logic},
   journal = {Studia Logica},
   publisher = {Springer Netherlands},
   keyword = {Humanities, Social Sciences and Law},
   pages = {23-34},
   volume = {33},
   issue = {1},
   year = {1974}
}

@InProceedings{Filinski92,
  author       = "Andrzej Filinski",
  title        = "Linear Continuations",
  booktitle    = "POPL",
  month        = jan,
  year         = 1992,
  publisher    = "ACM Press",
  pages        = "27--38",
}

@Unpublished{Reddy91,
  author       = "Udday S. Reddy",
  title        = "Acceptors as values: Functional programming in classical linear logic",
  note         = "Manuscript",
  year         = 1991,
  month        = dec,
  urlps        = "file://cs.uiuc.edu/pub/reddy/papers/acceptors.ps.Z",
  urldvi       = "file://cs.uiuc.edu/pub/reddy/papers/acceptors.dvi"
}

@TechReport{Naish,
        Author = {Lee Naish},
        Title = {Pruning in Logic Programming},
        Number = {95/16},
        Institution = {Department of Computer Science, University of
                  Melbourne},
        Address = {Melbourne, Australia},
        Month = jun,
        Year = 1995,
        url = "http://www.cs.mu.oz.au/~lee/papers/prune/",
}


@misc{HaskellList:MonadPlus,
  author =       {Benjamin C. Pierce and others},
  title =        {What is {M}onad\-{P}lus Good For?},
  howpublished = {\url{http://www.haskell.org/pipermail/haskell-cafe/2005-February/009072.html}},
  year =         2005,
  month = feb
}

@misc{HaskellList:Transaction,
  author =       {Remi Turk},
  title =        {What is {M}onad\-{P}lus Good For?},
  howpublished = {\url{http://www.haskell.org/pipermail/haskell-cafe/2005-February/009086.html}},
  year =         2005,
  month = feb
}

@misc{HaskellList:Failure,
  author =       {David Roundy},
  title =        {What is {M}onad\-{P}lus Good For?},
  howpublished = {\url{http://www.haskell.org/pipermail/haskell-cafe/2005-February/009081.html}},
  year =         2005,
  month = feb
}

@misc{HaskellList:SoftCut,
  author =       {Andrew Bromage},
  title =        {Initial (Term) Algebra for a State Monad},
  howpublished = {\url{http://www.haskell.org/pipermail/haskell-cafe/2005-January/008259.html}},
  year =         2005,
  month = jan
}

@Article{	spivey-combinators,
  author	= "J. Michael Spivey",
  title		= "Combinators for Breadth-First Search",
  journal	= "Journal of Functional Programming",
  year		= 2000,
  volume	= 10,
  number	= 4,
  pages		= "397--408"
}

@inproceedings{SeresSpivey,
  author	= "Silvija Seres and J. Michael Spivey",
  title = "Embedding {P}rolog in {H}askell",
  booktitle	= "Proceedings of the 1999 {H}askell Workshop",
  year = 1999,
  url		= "http://users.comlab.ox.ac.uk/silvija.seres/Papers/haskell99.ps.gz",
  editor =       {Erik Meier},
  publisher="Tech.\ Rep.\ UU-CS-1999-28, Department of Computer Science, Utrecht University"
}

@misc{HAWiki:MonadPlus,
  title = "{M}onad{P}lus",
  howpublished = {\url{http://www.haskell.org/hawiki/MonadPlus}},
  year = 2005
}

@misc{HAWiki:ListT,
  author = "Thomas Jaeger",
  title = "ListTDoneRight",
  howpublished = {\url{http://haskell.org/hawiki/ListTDoneRight}},
  year = 2004
}

@article{Zaniolo:ExpressiveNonDet,
  author = "Fosca Giannotti, Dino Pedreschi and Carlo Zaniolo",
  title = "Semantics and Expressive Power of Nondeterministic
Constructs in Deductive Databases",
  journal = "Journal of Computer and System Sciences",
  volume = 62,
  number = 1,
  year = 2001,
  pages = "15--42",
  url = "http://www.cs.ucla.edu/~zaniolo/papers/jcss01.pdf",
}

@InProceedings{tullsen00first,
    author = "Mark Tullsen",
    title = "First Class Patterns",
    pages = "1--15",
    year = "2000",
    editor = "Enrico Pontelli and V{\'\i}tor Santos Costa",
    booktitle = "Practical Aspects of Declarative Languages, 2nd International Workshop",
    volume = "1753",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    url = "http://link.springer.de/link/service/series/0558/papers/1753/17530001.pdf http://www.cs.yale.edu/homes/tullsen/patterns.ps"
}


@inproceedings{Hinze:deriving,
 author = {Ralf Hinze},
 title = {Deriving Backtracking Monad Transformers},
 booktitle = {{ICFP} '00: Proceedings of the 5th {ACM} {SIGPLAN} International Conference on Functional Programming},
 year = {2000},
 isbn = {1-58113-202-6},
 pages = {186--197},
 doi = {http://doi.acm.org/10.1145/351240.351258},
 publisher = {ACM Press}
 }

@article{VanRoy:WonderYears,
    author = "Peter Van Roy",
    title = "1983--1993: The Wonder Years of Sequential {P}rolog Implementation",
    journal = "Journal of Logic Programming",
    volume = "19--20",
    pages = "385--441",
    year = "1994",
    url = "citeseer.ist.psu.edu/vanroy93wonder.html" }

@InProceedings{ken,
  author =       {{Chung-chieh} Shan},
  title =        {Shift to Control},
  booktitle =    {Proceedings of the 5th workshop on {S}cheme and Functional Programming},
  pages =        {99-107},
  year =         2004,
  editor =       {Olin Shivers and Oscar Waddell},
  note =         {Technical report, Computer Science Department, Indiana University, 2004. }
}

@InProceedings{ahs04,
  author =       {Zena M. Ariola and Hugo Herbelin and Amr Sabry},
  title =        {A Type-Theoretic Foundation of Continuations and Prompts},
  pages = {40-53},
  booktitle =    icfp,
  year =         2004,
  publisher =    acm
}

@Unpublished{smlnjlib,
  key =        "SML/NJ Project",
  title =        {The {SML/NJ} Library},
  note =         {Available from \url{http://smlnj.org/}}
}

@inProceedings{ThieleckeESOP2000,
  author = "H. Thielecke",
  title = "On Exceptions versus Continuations in the Presence of State",
  booktitle = "Proceedings of the ninth European Symposium On Programming (ESOP)",
  publisher = "Springer-Verlag",
  series =  "Lecture Notes in Computer Science",
  volume =  "1782",
  pages = "397-411",
  year = "2000"
 }

@inProceedings{RieckeThieleckeICALP99,
  author = "J. G. Riecke and H. Thielecke",
  title = "Typed Exceptions and Continuations Cannot Macro-Express Each Other",
  booktitle = "Proceedings of the 26th International Colloquium on Automata,
               Languages and Programming (ICALP)",
  publisher = "Springer-Verlag",
  series =  "Lecture Notes in Computer Science",
  volume =  "1644",
  pages = "635-644",
  year = "1999"
 }



@InProceedings{Haynes:icolp:1986,
  author =       "Christopher T. Haynes",
  title =        "Logic Continuations",
  booktitle =    "Proceedings of the Third International Conference on
                 Logic Programming",
  publisher =    "Springer-Verlag",
  series =       "Lecture Notes in Computer Science",
  volume =       "225",
  pages =        "671-685",
  month =        jul,
  year =         "1986",
  keywords =     "continuations",
  reffrom =      "Rees:Clinger:acm:sigplan:1986",
  reffrom =      "Danvy:iait:1987",
  reffrom =      "Felleisen:acm:lfp:1988"
}


@Article{Haynes:Friedman:Wand:jocl:1986,
  author =       "C. T. Haynes and D. Friedman and M. Wand",
  title =        "Obtaining coroutines from continuations",
  journal =      "Journal of Computer Languages",
  volume =       "11",
  pages =        "143-153",
  year =         "1986",
  keywords =     "Scheme, continuations, coroutines",
  reffrom =      "Sitaram:Felleisen:acm:lfp:1990"
}

@Article{Wand:1999:CBMa,
  author =      "Mitchell Wand",
  title =       "Continuation-based multiprocessing",
  journal =     "Higher-Order and Symbolic Computation",
  year =        1999,
  volume =      12,
  number =      3,
  pages =       "285-299",
  note =        "\url{<http://www.brics.dk/~hosc/vol12/3-wand.html>}
                 Reprinted from the proceedings of the 1980 Lisp Conference,
                 with a foreword"
}

@Unpublished{thieleckestate,
  author =       {Hayo Thielecke},
  title =        {Contrasting Exceptions and Continuations},
  note =         {\url{http://www.cs.bham.ac.uk/~hxt/
                 research/exncontjournal.pdf}},
  year =         2001
}

@inproceedings{Moggi:1989:CLM,
 author = {Moggi, E.},
 title = {Computational lambda-calculus and monads},
 booktitle = {Symposium on Logic in Computer Science},
 series = {LICS},
 year = {1989},
 location = {Pacific Grove, California, United States},
 pages = {14--23},
 numpages = {10},
 publisher = {IEEE},
}

@article{Moggi:1991:NCM,
 author = {Moggi, Eugenio},
 title = {Notions of computation and monads},
 journal = {Inf. Comput.},
 volume = {93},
 issue = {1},
 month = {July},
 year = {1991},
 pages = {55--92},
 numpages = {38},
 publisher = {Academic Press, Inc.},
}

@inproceedings{317779,
 author = {Steven E. Ganz and Daniel P. Friedman and Mitchell Wand},
 title = {Trampolined style},
 booktitle = icfp,
 year = {1999},
 isbn = {1-58113-111-9},
 pages = {18-27},
 location = {Paris, France},
 doi = {http://doi.acm.org/10.1145/317636.317779},
 publisher = acm
 }

@TechReport{	felleisen-beyond,
  author	= "Matthias Felleisen and Daniel P. Friedman and Bruce F. Duba and John Merrill",
  title		= "Beyond Continuations",
  institution	= org_indiana_cs,
  year		= 1987,
  month		= feb,
  number	= 216
}

@article{198120,
 author = {Amr Sabry and Matthias Felleisen},
 title = {Reasoning about Programs in Continuation-Passing Style},
 journal = {Lisp and Symbolic Computation},
 volume = {6},
 number = {3-4},
 year = {1993},
 issn = {0892-4635},
 pages = {289-360},
 publisher = {Kluwer Academic Publishers}
 }

@InProceedings{	filinski-normalization,
  author	= "Andrzej Filinski",
  title		= "Normalization by Evaluation for the Computational Lambda-Calculus",
  pages		= "151--165",
  crossref	= "tlca2001",
  url		= "http://www.diku.dk/~andrzej/papers/NbEftCLC.dvi http://www.diku.dk/~andrzej/papers/NbEftCLC.ps.gz http://www.diku.dk/~andrzej/papers/NbEftCLC-abstract.html"
}

@InProceedings{	gasbichler-how,
  author	= "Martin Gasbichler and Eric Knauel and Michael Sperber and Richard A. Kelsey",
  title		= "How to Add Threads to a Sequential Language Without Getting Tangled Up",
  pages		= "30--47",
  crossref	= "scheme2003"
}

@Article{	grobauer-second,
  author	= "Bernd Grobauer and Zhe Yang",
  title		= "The Second {F}utamura Projection for Type-Directed Partial Evaluation",
  journal	= j_hosc,
  year		= 2001,
  volume	= 14,
  number	= "2--3",
  pages		= "173--219"
}

@InProceedings{	kiselyov-backtracking,
  author	= {Oleg Kiselyov and Shan, Chung-chieh and Daniel P. Friedman and Amr Sabry},
  title		= {Backtracking, Interleaving, and Terminating Monad Transformers (Functional Pearl)},
  pages		= "192--203",
  crossref	= "icfp2005"
}

@InProceedings{	lawall-continuation-based,
  author	= "Lawall, Julia L. and Danvy, Olivier",
  title		= "Continuation-Based Partial Evaluation",
  pages		= "227--238",
  crossref	= "lfp1994",
  url		= "http://www.diku.dk/users/julia/lawall-danvy-lfp94.ps.gz"
}

@InProceedings{	sewell-acute,
  author	= {Peter Sewell and James J. Leifer and Keith Wansbrough and Zappa Nardelli, Francesco and Mair Allen-Williams and Pierre Habouzit and Viktor Vafeiadis},
  title		= {Acute: High-Level Programming Language Design for Distributed Computation},
  pages		= "15--26",
  crossref	= "icfp2005",
  url		= "http://www.cl.cam.ac.uk/users/pes20/acute/acute2-short.ps http://www.cl.cam.ac.uk/users/pes20/acute/acute2-short.pdf"
}

@InProceedings{	sitaram-handling,
  author	= "Dorai Sitaram",
  title		= "Handling Control",
  pages		= "147--155",
  crossref	= "pldi1993",
  url		= "http://www.cs.rice.edu/CS/PLT/Publications/Scheme/pldi93-s.dvi.gz http://www.cs.rice.edu/CS/PLT/Publications/Scheme/pldi93-s.ps.gz"
}

@InProceedings{	sumii-implementation,
  author	= "Eijiro Sumii",
  title		= "An Implementation of Transparent Migration on Standard {S}cheme",
  pages		= "61--63",
  crossref	= "scheme2000",
  url		= "http://www.cis.upenn.edu/~sumii/pub/go.dvi http://www.cis.upenn.edu/~sumii/pub/go.ps.gz http://www.cis.upenn.edu/~sumii/pub/go.pdf"
}

@Article{	thiemann-combinators,
  author	= "Thiemann, Peter",
  title		= "Combinators for Program Generation",
  journal	= j_jfp,
  year		= 1999,
  volume	= 9,
  number	= 5,
  pages		= "483--525"
}


@Article{lillibridge,
  author =       {Mark Lillibridge},
  title =        {Unchecked Exceptions Can be Strictly More Powerful Than Call/CC},
  journal =      {Higher-Order and Symbolic Computation},
  year =         1999,
  volume =       12,
  number =       1,
  pages =        {75-104},
  month =        apr
}

@TechReport{control,
  author =       {R. Kent Dybvig and Peyton Jones, Simon L. and Amr Sabry},
  title =        {A Monadic Framework for Delimited Continuations},
  institution =  {Department of Computer Science, Indiana University},
  year =         2005,
  number =       {615},
  month =        jun
}

@article{Moreau,
 author = {Luc Moreau},
 title = {A Syntactic Theory of Dynamic Binding},
 journal = {Higher-Order and Symbolic Computation},
 volume = {11},
 number = {3},
 year = {1998},
 issn = {1388-3690},
 pages = {233-279},
 doi = {http://dx.doi.org/10.1023/A:1010087314987},
 publisher = {Kluwer Academic Publishers}
 }

@TechReport{	sabry-axiomatizing,
  author	= "Amr Sabry",
  title		= "Note on Axiomatizing the Semantics of Control Operators",
  institution	= "Department of Computer and Information Science, University of Oregon",
  year		= 1996,
  number	= "CIS-TR-96-03"
}

@InProceedings{KH:soucad,
  author =       "Yukiyoshi Kameyama and Masahito Hasegawa",
  title =        "A Sound and Complete Axiomatization of Delimited
                 Continuations",
  booktitle =    icfp,
  pages =        "177-188",
  publisher =    acm,
  year =         "2003"
}

@Article{WadlerPhil1994a,
  author =       "Philip Wadler",
  journal =      "Lisp and Symbolic Computation",
  title =        "Monads and composable continuations.",
  year =         1994,
  URL =          "ftp://ftp.dcs.gla.ac.uk/pub/glasgow-fp/authors/Philip_Wadler/monads-and-composable-continuations.dvi",
  month =        jan,
  number =       1,
  pages =        "39-56",
  volume =       7,
  scope =        "monads"
}

@inproceedings{Shan04,
    author = "Chung-Chieh Shan",
    title = "From shift and reset to polarized linear logic",
    year = "2004"
}

@inproceedings{ kameyama00typetheoretic,
    author = "Yukiyoshi Kameyama",
    title = "A Type-Theoretic Study on Partial Continuations",
    booktitle = "{IFIP} {TCS}",
    pages = "489-504",
    year = "2000",
    url = "citeseer.nj.nec.com/kameyama00typetheoretic.html" }

@inproceedings{Kameyama,
    author = "Yukiyoshi Kameyama",
    title = "Dynamic Control Operators in Type Theory",
    booktitle = "Unpublished manuscript",
    note = "Presented to the 2nd Asian Workshop on Programming Languages and Systems",
    year = 2001
}


@article{ hieb94subcontinuations,
    author = "Robert Hieb and Kent Dybvig and Claude W. {Anderson, {III}}",
    title = "Subcontinuations",
    journal = "Lisp and Symbolic Computation",
    volume = "7",
    number = "1",
    pages = "83-110",
    year = "1994",
    url = "citeseer.nj.nec.com/hieb93subcontinuations.html" }


@inproceedings{Murthy92,
  author = "Chetan R. Murthy",
  title = "Control Operators, Hierarchies, and Pseudo-Classical
           Type Systems: {A}-Translation at Work",
  booktitle = "ACM workshop on continuations",
  pages = "49-71",
  publisher	= org_stanford_cs,
  year		= 1992,
  number	= "STAN-CS-92-1426",
}

@inproceedings{GuzmanSuarez94,
  author = "J. Guzm\'an and A. Su\'arez",
  title = "An Extended Type System for Exceptions",
  booktitle = "Record of the fifth ACM SIGPLAN workshop on ML and its Applications",
  year = "1994",
  month = jun,
  note = "Also appears as Research Report 2265, INRIA,
                  BP 105 - 78153 Le Chesnay Cedex, France"
}


@inproceedings{ filinski94representing,
    author = "Andrzej Filinski",
    title = "Representing Monads",
    pages = "446-457",
  crossref	= "popl1994"
}

@article{Crolard04,
 author = {Tristan Crolard},
 title = {A formulae-as-types interpretation of subtractive logic},
 journal = {Journal of Logic and Computation (Special issue on Modalities in Constructive Logics and Type Theories)},
 year = {2004},
 note = {To appear},
 publisher = {Oxford University Press}
}

@article{Crolard01,
 author = {Tristan Crolard},
 title = {Subtractive logic},
 journal = {Theoretical Computer Science},
 volume = {254},
 number = {1-2},
 year = {2001},
 issn = {0304-3975},
 pages = {151-185},
 doi = {http://dx.doi.org/10.1016/S0304-3975(99)00124-3},
 publisher = {Elsevier Science Publishers Ltd.}
 }



@inproceedings{ kameyama-towards,
  author = "Yukiyoshi Kameyama",
  title = "Towards Logical Understanding of Delimited Continuations",
  booktitle = "Proceedings of the Third ACM SIGPLAN Workshop
               on Continuations (CW'01)",
  year = 2001
}

@inproceedings{ wadlericfp,
    author = "Philip Wadler",
    title = "The marriage of effects and monads",
    booktitle = icfp,
    volume = "34(1)",
    pages = "63-74",
    year = "1999"
}



@article{ Thielecke,
    author = "H. Thielecke",
    title = "Comparing Control Constructs by Double-barrelled {CPS} ",
    journal = "Higher-Order and Symbolic Computation",
    volume = "15",
    number = "2/3",
    pages = "119-136",
    year = "2002",
    publisher = "Kluwer"
}

@InProceedings{UserThreadsSCSH,
  title =        "Processes vs.\ User-Level Threads in {S}csh",
  author =       "Martin Gasbichler and Michael Sperber",
  crossref	= "scheme2002",
  url = {http://www-pu.informatik.uni-tuebingen.de/users/gasbichl/publications/scheme02.ps}
}

@Proceedings{	scheme2002,
  title		= "Proceedings of the 3rd Workshop on {S}cheme and Functional Programming",
  booktitle	= "Proceedings of the 3rd Workshop on {S}cheme and Functional Programming",
  year		= 2002,
  month		= "3~"  # oct,
  location	= "Pittsburgh, PA"
}

@misc{SRFI39,
 title = "Parameter objects",
 author = "Marc Feeley",
 year = 2003,
 howpublished = "{S}cheme {R}equest for {I}mplementation {SRFI}-39. \url{http://srfi.schemers.org/srfi-39/}",
 url="http://srfi.schemers.org/srfi-39/"
}

@Unpublished{Baker:Equal,
  author =       "Henry G. {Baker, Jr.}",
  title =        "Equal Rights for Functional Objects",
  year =         "1990",
  note =         "Submitted to {\em {ACM} Transactions on Programming
                 Languages and Systems}"
}


@article{ gasbichler-final,
  author = "Martin Gasbichler and Michael Sperber",
  title = "Final Shift for Call/cc: Direct Implementation of Shift and Reset",
  journal = "ACM SIGPLAN Notices",
  volume = "37",
  number = "9",
  pages = "271-282",
  year = "2002"
}

@inproceedings{ AH03,
    author = "Z. M. Ariola and H. Herbelin",
    title = "Minimal Classical Logic and Control Operators",
    booktitle = "Thirtieth International Colloquium on Automata, Languages and Programming , {ICALP}'03,
    Eindhoven, The Netherlands, June 30 - July 4, 2003",
    publisher = "Springer-Verlag, LNCS ",
    volume = "2719",
    pages = "871-885",
    year = "2003"
}

@article{Ariola:2009:TFD:1743339.1743381,
 author = {Ariola, Zena M. and Herbelin, Hugo and Sabry, Amr},
 title = {A type-theoretic foundation of delimited continuations},
 journal = {Higher Order Symbol. Comput.},
 volume = {22},
 issue = {3},
 month = {September},
 year = {2009},
 pages = {233--273},
 numpages = {41},
 publisher = {Kluwer Academic Publishers},
}

@inproceedings{FWFD88,
    author = "Matthias Felleisen and Mitchell Wand and Daniel P. Friedman and Bruce F. Duba",
    title = "Abstract continuations: A mathematical semantics for handling full functional jumps",
    booktitle ="Conference on LISP and Functional Programming, Snowbird, Utah",
    publisher = acm,
    pages = "52-62",
    year = "1988"
}


@article{ danvy92representing,
  author	= "Olivier Danvy and Andrzej Filinski",
  title		= "Representing Control: A Study of the {CPS} Transformation",
  journal	= j_mscs,
    volume = "2",
    number = "4",
    pages = "361-391",
    year = "1992",
  month		= dec
}

@article{ girard91,
    author = "J.-Y. Girard",
    title = " A New Constructive Logic: Classical Logic",
    journal = "Mathematical Structures in Computer Science",
    volume = "1",
    number = "3",
    pages = "255-296",
    year = "1991"
}

@techreport{ danvy89functional,
  author	= "Olivier Danvy and Andrzej Filinski",
    title = "A Functional Abstraction of Typed Contexts",
  institution	= org_diku,
  note		= "\url{http://www.daimi.au.dk/~danvy/Papers/fatc.ps.gz}",
    number = "89/12",
    months = aug,
    year = "1989"
}


@article{ queinnec93library,
    author = "C. Queinnec",
    title = "A Library of high-level control operators",
    journal = "ACM SIGPLAN Lisp Pointers",
    volume = "6",
    number = "4",
    pages = "11-26",
    year = "1993"
}

@INPROCEEDINGS{luc94partial,
  AUTHOR = {Luc Moreau and Christian Queinnec},
  TITLE = {Partial Continuations as the Difference of
		  Continuations: A Duumvirate of Control
		  Operators},
  volume = 844,
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {182-197},
  PAGECOUNT = {16},
  BOOKTITLE = {International  Conference  on  Programming  Language
		  Implementation and Logic Programming (PLILP'94)},
  YEAR = 1994,
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {Madrid, Spain},
  MONTH = SEP,
  URL = {http://www.ecs.soton.ac.uk/~lavm/papers/plilp94.ps.gz}
}

@inproceedings{ Queinnec91,
  author =       {Christian Queinnec and Bernard Serpette},
  title =        {A Dynamic Extent Control Operator for Partial Continuations},
  booktitle =    {Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '91)},
  month =        Jan,
  address =      {Orlando (Florida)},
  pages =        {174-184},
  year =         1991
}

@article{Bernardi:2010:CSL:1749618.1749689,
 author = {Bernardi, Raffaella and Moortgat, Michael},
 title = {Continuation semantics for the {L}ambek--{G}rishin calculus},
 journal = {Inf. Comput.},
 volume = {208},
 issue = {5},
 month = {May},
 year = {2010},
 pages = {397--416},
 numpages = {20},
 acmid = {1749689},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
}

@article{Abramsky:1994:NFG:184662.184664,
 author = {Abramsky, Samson and Jagadeesan, Radha},
 title = {New foundations for the geometry of interaction},
 journal = {Inf. Comput.},
 volume = {111},
 issue = {1},
 month = {May},
 year = {1994},
 pages = {53--119},
 numpages = {67},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
}

@Article{seventrees,
  author =       {A. Blass},
  title =        {Seven trees in one},
  journal =      {Journal of Pure and Applied Algebra},
  year =         1995,
  volume =    103,
  number =    {1-21}
}

@techreport{Rozas:1987:CMO:889539,
 author = {Rozas, Guillermo J},
 title = {A Computational Model for Observation in Quantum Mechanics},
 year = {1987},
 institution = {MIT},
 source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Amitai%3AMIT-AILab%2F%2FAITR-925},
 publisher = {Massachusetts Institute of Technology},
 address = {Cambridge, MA, USA},
}

@Article{transactional,
  author =       {John Cramer},
  title =        {The Transactional Interpretation of Quantum Mechanics},
  journal =      {Reviews of Modern Physics},
  year =         1986,
  volume =    58,
  pages =     {647-688}
}

@proceedings{DBLP:conf/rta/2005,
  editor    = {J{\"u}rgen Giesl},
  title     = {Term Rewriting and Applications, 16th International Conference,
               RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings},
  booktitle = {RTA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3467},
  year      = {2005},
}


@inproceedings{ danvy90abstracting,
  author	= "Olivier Danvy and Andrzej Filinski",
    title = "Abstracting Control",
    pages = "151-160",
  crossref	= "lfp1990"
}

@inproceedings{ barbanera93extracting,
    author = "F. Barbanera and S. Berardi",
    title = "Extracting Constructive Content from Classical Logic via Control-Like Reductions",
    booktitle = "Proceedings 1st International Conference on Typed Lambda Calculi and Applications, {TLCA}'93, Utrecht, The Netherlands, 16-18 March 1993",
    volume = "664",
    publisher = "Springer-Verlag",
    editor = "M. Bezem and J. F. Groote",
    pages = "45-59",
    year = "1993"
}

@phdthesis{ sitaram94models,
    author = "Dorai Sitaram",
    title = "Models of Control and Their Implications for Programming Language Design",
    school = "Rice University",
    pages = "166",
    year = "1994"
}

@inproceedings{ duba91typing,
    author = "B. F. Duba and R. Harper and D. MacQueen",
    title = "Typing First-Class Continuations in {ML}",
    booktitle = "Conference Record of the Eighteenth Annual {ACM} Symposium on Principles of Programming Languages",
    address = "Orlando, Florida",
    pages = "163-173",
    year = "1991"
}

@inproceedings{Groote94,
  AUTHOR = {P. de Groote},
  TITLE = {On the Relation between the lambda-mu  Calculus and the Syntactic Theory of Sequential Control},
  YEAR = 1994,
  BOOKTITLE = {Logic Programming and Automated Reasoning, Proceedings of the 5th International Conference, LPAR'94},
  EDITOR = {F. Pfennig},
  PUBLISHER = {Springer},
  PAGES = {31-43},
  KEYWORDS = {}}

@Article{Groote98,
  author       = "P. de Groote",
  title        = "An environment machine for the lambda-mu-calculus",
  journal      = "Mathematical Structures in Computer Science",
  year         = "1998",
  volume       = "8(6)",
  pages        = "637-669"
}

@Article{Crolard99,
  author       = "T. Crolard",
  title        = "A confluent lambda-calculus with a catch/throw mechanism",
  journal      = "Journal of Functional Programming",
  year         = "1999",
  volume       = "9(6)",
  pages        = "625-647"
}

@Article{Streicher98,
  author       = "T. Streicher and B. Reus",
  title        = "Classical logic: Continuation Semantics and Abstract Machines",
  journal      = "Journal of Functional Programming",
  year         = "1998",
  volume       = "8(6)",
  pages        = "543-572"
}


@InCollection{howard,
  author =       "W. Howard",
  title =        "The formulae-as-types notion of construction",
  booktitle =    "To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism",
  publisher =    "Academic Press",
  year =         1980,
  editor =       "J. R. Hindley and J. P. Seldin",
  pages =        "479-490"
}

@book{cuf,
        author = {H. B. Curry and R. Feys},
        title = {Combinatory Logic, Volume I},
        publisher = "North-Holland",
        address = "Amsterdam",
        year = 1958
}

@book{lalement93,
        author = {Ren{\'e} Lalement},
        title = {Computation as Logic},
        publisher = "Prentice Hall International Series in Computer Science",
        address = "Amsterdam",
        year = 1993
}

@book{girard89,
        author = {J.Y. Girard and P. Taylor and Y. Lafont},
        title = {Proofs and Types},
        publisher = "Cambdrige University Press",
        year = 1989
}

@Book{Prawitz,
  author =       "D. Prawitz",
  title =        "Natural Deduction, a Proof-Theoretical Study",
  publisher =    "Almquist and Wiksell, Stockholm",
  year = "1965"
}

@incollection{gentzen35,
  author =       "G. Gentzen",
  title =        "Investigations into logical deduction",
  booktitle = "Collected papers of Gerhard Gentzen",
  editor = " M.E. Szabo",
  pages  = "68-131",
  publisher =    "North-Holland",
  year = "1969"
}

@article{Girard87tcs,
  author       = "J.-Y. Girard",
  title        = "Linear Logic",
  journal      = "Theor. Comput. Sci.",
  year         = 1987,
  volume       = 50,
  pages        = "1-102"
}

@inproceedings{Felleisen86a,
  author       = "M. Felleisen and D. Friedman and E. Kohlbecker and B. Duba",
  title        = "Reasoning with continuations",
  booktitle = "First Symposium on Logic and Computer Science",
  pages        = "131-141",
  year         = "1986"
}

@article{ felleisen92revised,
    author = "M. Felleisen and R. Hieb",
    title = "The Revised Report on the Syntactic Theories of Sequential Control and State",
    journal = "Theoretical Computer Science",
    volume = "103",
    number = "2",
    pages = "235-271",
    year = "1992"
}

@inproceedings{Hieb90,
  author       = "R. Hieb and R. K. Dybvig",
  title        = "Continuations and cuncurrency",
  booktitle    = "Second ACM SIGPLAN symposium on principles \& practice of
                  parallel programming",
  publisher   = acm,
  pages        = "128-136",
  year         = "1990"
}

@inproceedings{Felleisen86b,
  author       = "M. Felleisen and D. Friedman",
  title        = "Control operators, the secd machine, and the lambda-calculus",
  booktitle = "Formal description of programming concepts-III",
  publisher   = "North-Holland",
  pages        = "193-217",
  year         = "1986"
}

@Article{	felleisen-expressive,
  author	= "Matthias Felleisen",
  title		= "On the Expressive Power of Programming Languages",
  journal	= j_scp,
  year		= 1991,
  volume	= 17,
  number	= "1--3",
  pages		= "35--75"
}

@incollection{ barendregt92lambda,
    author = "Barendregt",
    title = "Lambda Calculi with Types",
    booktitle = "Handbook of Logic in Computer Science",
    editor = "Abramsky \& Gabbay \& Maibaum",
    volume = "2",
    year = "1992"
}


@phdthesis{ geuvers93logics,
    author = "Herman Geuvers",
    title = "Logics and Type Systems",
    school = "Nijmegen University",
    year = "1993"
}

@phdthesis{ walterpy98,
    author = "W. Py ",
    title = "Confluence en $\lambda\mu$-calcul",
    school = "Universit\'e de Savoie",
    year = "1998"
}

@book{ nordstrom90programming,
  author = "B. Nordstrom and K. Petersson and J. Smith",
  title = "Programming in Martin-L{\"o}f's Type Theory: An Introduction",
  publisher = " Clarendon Press, Oxford" ,
  year = "1990" }


@inproceedings{ coquand94inductive,
    author = "T. Coquand and P. Dybjer",
    title = "Inductive Definitions and Type Theory: an Introduction (Preliminary Version)",
    booktitle = "Foundations of Software Technology and Theoretical Computer Science",
    pages = "60-76",
    year = "1994"
}

@inproceedings{ coquand88inductively,
    author = "T. Coquand and C. Paulin",
    title = "Inductively defined types",
    booktitle = "Conference on Computer Logic",
    pages = "50-66",
    year = "1988"
}

@inproceedings{ Prehofer-CADE1994,
        author = {Christian Prehofer},
        title = {Decidable Higher-Order Unification Problems},
        booktitle = {Automated Deduction CADE-12, 12th International Conference on Automated Deduction},
        year = {1994},
        publisher = {Springer}
}

@inproceedings{ dowek95higherorder,
    author = "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner",
    title = "Higher-Order Unification via Explicit Substitutions",
    booktitle = "Proceedings of the Tenth Annual Symposium on Logic in Computer Science",
    month = jun,
    publisher = "IEEE Computer Society Press",
    address = "San Diego, California",
    editor = "D. Kozen",
    pages = "366-374",
    year = "1995"
}

@inproceedings{ pfenning91unification,
  author = "F. Pfenning",
  title = "Unification and anti-unification in the calculus of constructions",
  booktitle = "In Symp. Logic in Computer Science",
  pages = "74-85",
  year = "1991" }

@inproceedings{ necula97:proof-carrying-code,
  author =       {George C. Necula},
  title =        {Proof-Carrying Code},
  booktitle =    {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '97)},
  month =        Jan,
  address =      {Paris},
  pages =        {106-119},
  year =         1997
}

@inproceedings{ necula98design,
  author = "G. Necula and P. Lee",
  title = "The design and implementation of a certifying compiler",
  booktitle ="Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
  pages = "333-344",
  editor =" Keith D. Cooper",
  month = jun,
  year = "1998"
}



@inproceedings{ morrisett97from,
    author = "G. Morrisett and D. Walker and K. Crary and N. Glew",
    title = "From System {F} to Typed Assembly Language (Extended Version)",
    booktitle ={Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98)},
    month = jan,
    pages = "85-97",
    year = "1998"
}

@InProceedings{ gunter95generalization,
  author =       "Carl A. Gunter and Didier R{\'e}my and Jon G. Riecke",
  title =        "A Generalization of Exceptions and Control in
                 {ML}-Like Languages",
  booktitle =    "Functional Programming Languages and Computer Architecture: 7th Conference",
  year =         "1995",
  month		= "26--28 "  # jun,
  editor	= "Peyton Jones, Simon L.",
  URL =          "ftp://ftp.research.att.com/dist/riecke/prompt.ps.gz",
  publisher =    acm,
  pages = "12-23"
}

@Article{Felleisen87,
  author       = "M. Felleisen and D. Friedman and E. Kohlbecker",
  title        = "A syntactic theory of sequential control",
  journal      = "Theoretical Computer Science",
  year         = "1987",
  volume       = "52(3)",
  pages        = "205-237"
}

@PhDThesis{	felleisen-calculi,
  author	= "Matthias Felleisen",
  title		= "The Calculi of $\lambda_v$-{CS} Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages",
  school	= org_indiana_cs,
  year		= 1987,
  month		= aug,
  note		= "Also as "  # techreport # " 226"
}

@inproceedings{ felleisen88,
    author = "Matthias Felleisen",
    title = "The Theory and Practice of First-Class Prompts",
  crossref	= "popl1988",
    pages = "180-190"
}

@Article{Sitaram:Felleisen:lasc:1990,
  author =       "Dorai Sitaram and Matthias Felleisen",
  title =        "Control delimiters and their hierarchies",
  journal =      "Lisp and Symbolic Computation",
  volume =       "3",
  number =       "1",
  pages =        "67-99",
  year =         "1990"
}

@Article{Fischer:LaSC93,
  author =      "Michael J. Fischer",
  title =       "Lambda-Calculus Schemata",
  pages =       "259-288",
  journal =     "LISP and Symbolic Computation",
  year =        1993,
  volume =      6,
  number =      "3/4",
  note =        "\url{<http://www.brics.dk/~hosc/vol06/03-fischer.html>}
                 Earlier version available in the proceedings
                 of an ACM Conference on Proving Assertions about Programs,
                 SIGPLAN Notices, Vol.~7, No.~1, January 1972"
}


@InProceedings{Fischer72,
  author =       {Michael J. Fischer},
  title =        {Lambda-calculus schemata},
  booktitle =    {Proc. ACM Conference on Proving Assertions About Programs},
  series =       {SIGPLAN Notices},
  volume =       "7(1)",
  publisher =    acm,
  pages =        {104-109},
  year =         1972
}

@InProceedings{HiDy90,
  author =       "Robert Hieb and R. Kent Dybvig",
  title =        "{Continuations and Concurrency}",
  booktitle =    "PPoPP '90, Symposium on Principles and Practice of
                 Parallel Programming",
  address =      "Seattle, Washington, March 14-16",
  year =         "1990",
  series =       "SIGPLAN NOTICES",
  volume =       "25(3)",
  publisher =    acm,
  pages =        "128-136"
}

@inproceedings{Buhrman:2001:TSB:646254.684114,
 author = {Buhrman, Harry and Tromp, John and Vit\'{a}nyi, Paul M. B.},
 title = {Time and Space Bounds for Reversible Simulation},
 booktitle = {International Colloquium on Automata, Languages and Programming,},
 year = {2001},
 pages = {1017--1027},
 numpages = {11},
 acmid = {684114},
 publisher = {Springer-Verlag},
}

@inProceedings{ griffin90formulaeastypes,
    author = "Timothy G. Griffin",
    title = "The Formulae-as-Types Notion of Control",
    booktitle = popl,
    publisher = acm,
    pages = "47-57",
    year = "1990"
}

@article{ parigot93classical,
  author = "M. Parigot",
  title = "Classical proofs as programs",
  journal = "Computational logic and theory",
  volume = "713",
  pages = " 263-276",
  year = "1993"
}

@inProceedings{parigot92classical,
    author = "M. Parigot",
    title = "Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction",
    booktitle = "Logic Programming and Automated Reasoning:
                 International Conference LPAR '92 Proceedings, St. Petersburg, Russia",
    publisher = "Springer-Verlag",
    pages = "190-201",
    year = "1992"
}

@inProceedings{ murthy91evaluation,
  author = "C. Murthy",
  title = "An Evaluation Semantics for Classical Proofs",
  booktitle = "Proc. 6th Annual IEEE Symposium on Logic in Computer Science" ,
  pages =  "96 - 107",
  year = "1991" }



@inproceedings{ herbelin94calculus,
  author = "H. Herbelin",
  title = "A lambda-calculus structure isomorphic to {G}entzen-style sequent calculus structure",
  booktitle = "Proc. Annual Conference of the European Association
    for Computer Science Logic, Kazimierz, Poland, (Springer Verlag LNCS 933",
  year = "1994" }

@article{Herbelin01,
    author = {Hugo Herbelin},
    title = {Explicit Substitutions and Reducibility},
    journal = {Journal of Logic and Computation},
    pages = {431-451},
    publisher = acm,
    volume = {11},
    number ={3},
    year = {2001}
}

@inproceedings{ constable71constructive,
  author = "R. Constable",
  title = "Constructive mathematics and automatic program writers",
  booktitle = "In Proceedings of the IFIP Congress",
  pages = "229-233",
  publisher = "NorthHolland",
  year = "1971"
}


@article{ krivine90programming,
    author = "Krivine and M. Parigot",
    title = "Programming with Proofs",
    journal = "EIK: Journal of Information Processing and Cybernetics EIK (formerly Elektronische Informationsverarbeitung und Kybernetik)",
    volume = "26",
    year = "1990"
}


@article{ hyland00full,
    author = "J. M. E. Hyland and C.-H. Luke Ong",
    title = "On Full Abstraction for {PCF}: I, {II}, and {III}",
    journal = "Information and Computation",
    volume = "163",
    number = "2",
    pages = "285-408",
    year = "2000"
}

@inproceedings{ HS97,
    author = "M. Hofman and T. Streicher",
    title = "Continuation models are universal for lambda-$\mu$-calculus",
    booktitle = "Proceedings 12th Annual {IEEE}
                 Symp.\ on Logic in Computer Science, {LICS}'97, Warsaw, {Poland}, July 29- August 02 1997",
    publisher = "IEEE Computer Society Press",
    pages = "387-398",
    year = "1997"
}


@inproceedings{ ong96semantic,
    author = "C.-H. Luke Ong",
    title = "A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract)",
    booktitle = "Logic in Computer Science, {LICS}",
    publisher = "IEEE Computer Society Press",
    address = "Los Alamitos, CA",
    pages = "230-241",
    year = "1996"
}

@inproceedings{ ong97curryhoward,
    author = "C.-H. Luke Ong and C. A. Stewart",
    title = "A {C}urry-{H}oward Foundation for Functional Computation with Control",
    booktitle = popl,
    publisher = acm,
    pages = "215-227",
    year = "1997"
}


@inproceedings{ abramsky94full,
  author = "S. Abramsky and R. Jagadeesan and P. Malacaria",
  title = "Full Abstraction for {PCF}",
  booktitle = "Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS'94)",
  publisher = "Springer-Verlag",
  editor = "Masami Hagiya and John C. Mitchell",
  pages = "1-15",
  month = apr,
  year = "1994"
}

@inproceedings{ nickau94hereditarily,
    author = "H. Nickau",
    title = "Hereditarily Sequential Functionals",
    booktitle = "Proceedings of the Symposium on Logical Foundations of Computer Science: Logic at St.\ Petersburg",
    publisher = "Springer",
    year = "1994"
}


@inproceedings{ curien98computing,
    author = "P.-L. Curien and Hugo Herbelin",
    title = "Computing with Abstract Bohm Trees",
    booktitle = "Fuji International Symposium on Functional and Logic Programming",
    pages = "20-39",
    year = "1998"
}


@article{ Girardludics,
  author       = "J.-Y. Girard",
  title = "LOCUS SOLUM: From the rules of logic to the logic of rules",
  journal = "Mathematical Structures in Computer Science ",
  notes = "To appear",
  year = "2001" }


@incollection{ barendregt01proofassistants,
    author = "Henk Barendregt and Herman Geuvers",
    title = "Proof-Assistants Using Dependent Type Systems",
    booktitle = "Handbook of Automated Reasoning",
    pages = "1149-1238",
    year = "2001"
}

@inproceedings{ sitaram90reasoning,
    title = "Reasoning with Continuations {II}: Full Abstraction for Models of Control",
 author = {Dorai Sitaram and Matthias Felleisen},
 crossref="lfp1990",
 pages = {161--175},
 location = {Nice, France}
 }

@inproceedings{ barthe97notion,
    author = "Gilles Barthe and John Hatcliff and Morten Heine S{\o}rensen",
    title = "A Notion of Classical Pure Type Systems",
    booktitle = "Mathematical foundations of programming semantics",
    volume = "6",
    publisher = "Elsevier",
    editor = "S. Brookes and M. Main and A. Melton and M. Mislove",
    year = "1997"
}

@inproceedings{ bierman98,
    author = "G.M. Bierman",
    title = "A Computational Interpretation of the lambda-mu calculus",
    booktitle = "Mathematical foundations of computer science semantics,
                 LNCS 1450",
    publisher = "Springer-Verlag",
    editor = "L. Brim and J. Gruska and J. Zlatuska ",
    pages = " 336-345",
    year = "1998"
}

@INPROCEEDINGS{Miq00b,
  author = {Alexandre Miquel},
  title = {A Model for Impredicative Type Systems with Universes,
                  Intersection Types and Subtyping},
  booktitle = {Proceedings of the 15th Annual IEEE Symposium on Logic
                  in Computer Science (LICS'00)},
  year = {2000}
}


@article{ danos95new,
    author = "Vincent Danos and Jean-Baptiste Joinet and Harold Schellinx",
    title = "A New Deconstructive Logic: Linear Logic",
    journal = "Journal of Symbolic Logic",
    volume = "62",
    number = "3",
    pages = " 755-807",
    year = "1995"
}


@article{ Rauszer74,
    author = "Cecylia Rauszer",
    title = "Semi-boolean algebras and their application to intuitionistic logic with dual connectives",
    journal = "Fundamenta Mathematicae",
    volume = "83",
    pages = " 219-249",
    year = "1974"
}


@TechReport{	moggi-abstract,
  author	= "Eugenio Moggi",
  title		= "An Abstract View of Programming Languages",
  institution	= org_edinburgh_lfcs,
  year		= 1990,
  number	= "ECS-LFCS-90-113",
  url		= "http://www.disi.unige.it/person/MoggiE/ftp/abs-view.ps.gz"
}


@InProceedings{siskind-nondeterministic,
    title="Nondeterministic {L}isp as a Substrate for Constraint Logic Programming",
    author="Jeffrey Mark Siskind and David Allen McAllester",
    pages="133--138",
  booktitle	= "{AAAI}-93: Proceedings of the 11th National Conference on Artificial Intelligence",
  publisher	= "{AAAI} Press",
  year		= 1993,
  month="11--15 "#jul
}

@InProceedings{	wadler-essence,
  author	= "Philip L. Wadler",
  title		= "The Essence of Functional Programming",
  pages		= "1--14",
  year		= 1992,
  isbn		= "0-89791-453-8",
  booktitle ={{POPL} '92: Proceedings of the 19th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
 publisher = {ACM Press}
}

@Article{	wadler-comprehending,
  author	= "Philip L. Wadler",
  title		= "Comprehending Monads",
  journal	= "Mathematical Structures in Computer Science",
  year		= 1992,
  volume	= 2,
  number	= 4,
  pages		= "461--493"
}

@Misc{kanren,
  author =       {Oleg Kiselyov},
  title =        {A Declarative Applicative Logic Programming System},
  howpublished = {\url{http://kanren.sourceforge.net/}},
  year =         2004
}

@InProceedings{	cobbe-environmental,
  author	= "Richard Cobbe and Matthias Felleisen",
  title		= "Environmental Acquisition Revisited",
  crossref	= "popl2005",
  pages="14--25"
}

@Proceedings{	popl2005,
  key		= "{\relax POPL}",
  title		= popl,
  booktitle	= popl,
  publisher	= pub_acm,
  year		= 2005,
  location	= {Long Beach, CA}
}

@Article{lorenz,
  author =       {Lorenz Huelsbergen},
  title =        {A Logically Reversible Evaluator for the Call-by-name Lambda Calculus},
  journal =      {InterJournal Complex Systems},
  year =         1996,
  volume =       46
}

@InProceedings{	gil-environmental,
  author	= {Joseph Gil and David H. Lorenz},
  title		= {Environmental Acquisition---A New Inheritance{\hyp}Like Abstraction Mechanism},
  pages		= "214--231",
  crossref	= {oopsla1996}
}

@Proceedings{	oopsla1996,
  key		= "{\relax OOPSLA}",
  title		= "Proceedings of the 11th Conference on Object-Oriented Programming Systems, Languages, and Applications",
  booktitle	= "Proceedings of the 11th Conference on Object-Oriented Programming Systems, Languages, and Applications",
  publisher	= pub_acm,
  year		= 1996,
  month		= "6--10 "  # oct,
  volume	= "31(10)",
  series	= j_sigplan,
  isbn		= "0-201-92109-X",
  location	= {San Jose, California}
}

@InProceedings{	clements-tail-recursive,
  author	= "John Clements and Matthias Felleisen",
  title		= "A Tail-Recursive Semantics for Stack Inspections",
  pages		= "22--37",
  crossref	= "esop2003"
}

@Proceedings{	esop2003,
  editor	= "Pierpaolo Degano",
  title		= "Programming Languages and Systems: Proceedings of {ESOP} 2003, 12th {E}uropean Symposium on Programming",
  booktitle	= "Programming Languages and Systems: Proceedings of {ESOP} 2003, 12th {E}uropean Symposium on Programming",
  publisher	= pub_sv,
  year		= 2003,
  number	= 2618,
  series	= s_lncs,
  isbn		= "3-540-00886-1",
  location	= "Warsaw"
}

@Article{	haynes-embedding,
  author	= "Christopher T. Haynes and Daniel P. Friedman",
  title		= "Embedding Continuations in Procedural Objects",
  journal	= j_toplas,
  year		= 1997,
  month		= oct,
  volume	= 9,
  number	= 4,
  pages		= "582--598"
}

@InProceedings{	launchbury-lazy,
  author	= "John Launchbury and Peyton Jones, Simon L.",
  title		= "Lazy Functional State Threads",
  pages		= "24--35",
  crossref	= "pldi1994"
}

@Proceedings{	pldi1994,
  key		= "{\relax PLDI}",
  title		= pldi,
  booktitle	= pldi,
  publisher	= pub_acm,
  year		= 1994,
  volume	= "29(6)",
  series	= j_sigplan,
  location	= "Orlando, FL"
}

@Article{	launchbury-state,
  author	= "John Launchbury and Peyton Jones, Simon L.",
  title		= "State in {H}askell",
  journal	= j_lsc,
  year		= 1995,
  month		= dec,
  volume	= 8,
  number	= 4,
  pages		= "293--341"
}

@Misc{		gunter-return,
  author	= "Carl A. Gunter and Didier R{\'e}my and Jon G. Riecke",
  title		= "Return Types for Functional Continuations",
  year		= 1998,
  month		= sep,
  howpublished	= "\url{http://pauillac.inria.fr/~remy/work/cupto/}",
  url		= "http://pauillac.inria.fr/~remy/work/cupto/cupto.ps.gz http://pauillac.inria.fr/~remy/work/cupto/cupto.dvi.gz"
}

@InProceedings{	cartwright-extensible,
  author	= "Robert Cartwright and Matthias Felleisen",
  title		= "Extensible Denotational Language Specifications",
  pages		= "244--272",
  crossref	= "tacs1994",
  url		= "http://www.ccs.neu.edu/scheme/pubs/ http://www.ccs.neu.edu/scheme/pubs/tacs94-cf.dvi.gz http://www.ccs.neu.edu/scheme/pubs/tacs94-cf.ps.gz"
}

@Proceedings{	tacs1994,
  editor	= "Masami Hagiya and John C. Mitchell",
  title		= "Theoretical Aspects of Computer Software: International Symposium",
  booktitle	= "Theoretical Aspects of Computer Software: International Symposium",
  publisher	= pub_sv,
  year		= 1994,
  number	= 789,
  series	= s_lncs,
  location	= "Sendai, Japan"
}

@Proceedings{	lfp1990,
  key		= "{\relax LFP}",
  title		= "Proceedings of the {ACM} Conference on {L}isp and Functional Programming",
  booktitle	= "Proceedings of the {ACM} Conference on {L}isp and Functional Programming",
  publisher	= pub_acm,
  year		= 1990,
  month		= "27--29 "#jun,
  location	= "Nice, France"
}

@Proceedings{	lopstr2003,
  editor	= "Maurice Bruynooghe",
  title		= "{LOPSTR} 2003: 13th International Symposium on Logic Based Program Synthesis and Transformation",
  booktitle	= "{LOPSTR} 2003: 13th International Symposium on Logic Based Program Synthesis and Transformation",
  publisher	= pub_sv,
  year		= 2004,
  number	= 3018,
  series	= s_lncs,
  isbn		= {3-540-22174-3},
  location	= "Uppsala, Sweden"
}

@Proceedings{	appsem2000,
  editor	= "Gilles Barthe and Peter Dybjer and Luis Pinto and Jo{\~a}o Saraiva",
  title		= "{APPSEM} 2000: International Summer School on Applied Semantics, Advanced Lectures",
  booktitle	= "{APPSEM} 2000: International Summer School on Applied Semantics, Advanced Lectures",
  publisher	= pub_sv,
  year		= 2002,
  number	= 2395,
  series	= s_lncs,
  isbn		= {3-540-44044-5},
  location	= {Caminha, Minho, Portugal}
}

@Proceedings{	popl1988,
  key		= "{\relax POPL}",
  title		= popl,
  booktitle	= popl,
  publisher	= pub_acm,
  year		= 1988,
  month=jan,
  isbn		= {0-89791-252-7},
  location	= {San Diego, CA}
}

@Proceedings{	popl1994,
  key		= "{\relax POPL}",
  title		= popl,
  booktitle	= popl,
  publisher	= pub_acm,
  year		= 1994,
  isbn		= "0-89791-636-0",
  issn		= "0730-8566",
  location	= "Portland, OR"
}

@Proceedings{	gpce2002,
  editor	= "Don S. Batory and Charles Consel and Walid Taha",
  title		= "{ACM} {SIGPLAN}\slash{SIGSOFT} Conference on Generative Programming and Component Engineering",
  booktitle	= "{ACM} {SIGPLAN}\slash{SIGSOFT} Conference on Generative Programming and Component Engineering",
  publisher	= pub_sv,
  year		= 2002,
  number	= 2487,
  series	= s_lncs,
  url		= "http://link.springer.de/link/service/series/0558/tocs/t2487.htm http://www.springerlink.com/link.asp?id=kyuyqernba7e http://www.springerlink.com/openurl.asp?genre=issue&issn=0302-9743&volume=2487",
  isbn		= {3-540-44284-7}
}

@Proceedings{	icfp2005,
  key		= "{\relax ICFP}",
  title		= icfp,
  booktitle	= icfp,
  publisher	= pub_acm,
  year		= 2005,
  location	= "Tallinn"
}

@Proceedings{	lfp1994,
  key		= "{\relax LFP}",
  title		= "Proceedings of the {ACM} Conference on {L}isp and Functional Programming",
  booktitle	= "Proceedings of the {ACM} Conference on {L}isp and Functional Programming",
  publisher	= pub_acm,
  year		= 1994,
  location	= "Orlando, FL"
}

@Proceedings{	pldi1993,
  key		= "{\relax PLDI}",
  title		= pldi,
  booktitle	= pldi,
  publisher	= pub_acm,
  year		= 1993,
  month		= jun,
  issn		= "0362-1340",
  location	= "Albuquerque"
}

@Proceedings{	popl2004,
  key		= "{\relax POPL}",
  title		= popl,
  booktitle	= popl,
  publisher	= pub_acm,
  year		= 2004,
  location	= {Venice, Italy}
}

@Proceedings{	scheme2000,
  editor	= "Matthias Felleisen",
  title		= "Proceedings of the Workshop on {S}cheme and Functional Programming",
  booktitle	= "Proceedings of the Workshop on {S}cheme and Functional Programming",
  publisher	= org_rice_cs,
  year		= 2000,
  month		= sep,
  number	= "00-368",
  series	= techreport,
  url		= "http://www.ccs.neu.edu/home/matthias/Scheme2000/",
  location	= montreal
}

@Misc{		kiselyov-general,
  author	= "Oleg Kiselyov",
  title		= "General Ways to Traverse Collections",
  year		= 2004,
  month		= "1~"  # jan,
  howpublished	= "\url{http://okmij.org/ftp/Scheme/enumerators-callcc.html}; \url{http://okmij.org/ftp/Computation/Continuations.html}",
  url		= "http://okmij.org/ftp/Scheme/enumerators-callcc.html"
}

@Article{	queinnec-web,
  author	= "Christian Queinnec",
  title		= "Continuations and Web Servers",
  journal	= j_hosc,
  year		= 2004,
  month		= dec,
  volume	= 17,
  number	= 4,
  pages		= "277--295",
}

@PhDThesis{	graunke-web,
  author	= "Paul Thorsen Graunke",
  title		= "Web Interactions",
  school	= org_neu_cs,
  year		= 2003,
  month		= jun
}

@PhDThesis{	smith-reflection,
  author	= "Brian Cantwell Smith",
  title		= "Reflection and Semantics in a Procedural Language",
  school	= org_mit_eecs,
  year		= 1982,
  month		= feb,
  note		= "Also as "  # techreport # " MIT/LCS/TR-272",
  url		= "http://www.lcs.mit.edu/publications/specpub.php?id=840 http://www.lcs.mit.edu/publications/pubs/pdf/MIT-LCS-TR-272.pdf",
}

@InProceedings{	danvy-intensions,
  author	= "Olivier Danvy and Karoline Malmkj{\ae}r",
  title		= "Intensions and Extensions in a Reflective Tower",
  pages		= "327--341",
  crossref	= "lfp1988",
  url		= "http://www.daimi.au.dk/~danvy/research.html",
  keywords	= "procedural reflection, reification, meta-continuation, Blond, tail-reflection, single-threadedness, jumpy and pushy continuations"
}

@Proceedings{	lfp1988,
  key		= "{\relax LFP}",
  title		= "Proceedings of the {ACM} Conference on {L}isp and Functional Programming",
  booktitle	= "Proceedings of the {ACM} Conference on {L}isp and Functional Programming",
  publisher	= pub_acm,
  year		= 1988,
  isbn		= {0-89791-273-X},
  location	= "Snowbird, UT"
}

@Article{	wand-mystery,
  author	= "Mitchell Wand and Daniel P. Friedman",
  title		= "The Mystery of the Tower Revealed: A Non-Reflective Description of the Reflective Tower",
  journal	= j_lsc,
  year		= 1988,
  volume	= 1,
  number	= 1,
  pages		= "11--37",
  url="http://www.brics.dk/~hosc/vol01/01-wand-friedman.html http://www.brics.dk/~hosc/local/LaSC-1-1-pp11-37.pdf",
}

@Proceedings{	scheme2005,
  editor	= "J. Michael Ashley and Michael Sperber",
  title		= "Proceedings of the 6th Workshop on {S}cheme and Functional Programming",
  booktitle	= "Proceedings of the 6th Workshop on {S}cheme and Functional Programming",
  publisher	= org_indiana_cs,
  year		= 2005,
  month		= "24~"  # sep,
  number	= 619,
  series	= techreport,
  url		= "http://www.deinprogramm.de/scheme-2005/scheme-2005-proceedings.pdf",
  location	= "Tallinn"
}

@Manual{acl,
    title="{A}llegro {C}ommon {L}isp 8.0",
    organization="Franz Inc.",
    year=2006,month="17~"#mar
}

@Article{baker-shallow,
    title="Shallow Binding in {L}isp 1.5",
    author="Henry G. Baker",
    journal="Communications of the ACM",
    volume=21,number=7,month=jul,year=1978,pages="565--569",
    url="http://home.pipeline.com/~hbaker1/ShallowBinding.html http://home.pipeline.com/~hbaker1/ShallowBinding.ps.gz"
}

@Misc{matthews-learned,
    author="Jacob Matthews",
    title="{I} Learned Today That {PLT} {S}cheme Actually Has {\it Two\/} Kinds of Thread-Local Storage Boxes",
    year=2005,month="26~"#aug,
    howpublished="\url{http://keepworkingworkerbee.blogspot.com/2005/08/i-learned-today-that-plt-scheme.html}"
}

@TechReport{	bawden-reification,
  author	= "Bawden, Alan",
  title		= "Reification without Evaluation",
  institution	= org_mit_ai,
  year		= 1988,
  month		= "1~"  # jun,
  type		= "Memo",
  number	= 946,
  url		= "https://dspace.mit.edu/handle/1721.1/6461",
}

@Article{	baker-arrays,
  author	= "Henry G. Baker",
  title		= "Shallow Binding Makes Functional Arrays Fast",
  journal	= j_sigplan,
  year		= 1991,
  month		= aug,
  volume	= 26,
  number	= 8,
  pages		= "145--147",
  url		= "http://home.pipeline.com/~hbaker1/ShallowArrays.html http://home.pipeline.com/~hbaker1/ShallowArrays.ps.gz"
}

@Article{vanTonder:2004,
  author =       {A. van Tonder},
  title =        {A Lambda Calculus for Quantum Computation},
  journal =      {SIAM Journal on Computing},
  year =         2004,
  volume =       33,
  number =       5,
  pages =        {1109-1135}
}

@PhdThesis{duncan,
  author =       {R. Duncan},
  title =        {Types for quantum computation},
  school =       {Oxford University},
  year =         2006
}

@article{DBLP:journals/mscs/SelingerV06,
  author    = {Peter Selinger and
               Beno\^{\i}t Valiron},
  title     = {A lambda calculus for quantum computation with classical control},
  journal   = {MSCS},
  volume    = {16},
  number    = {3},
  year      = {2006},
  pages     = {527-552},
  ee        = {http://dx.doi.org/10.1017/S0960129506005238},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Filinski:1989:DCI:648332.755574,
 author = {Filinski, Andrzej},
 title = {Declarative Continuations: an Investigation of Duality in Programming Language Semantics},
 booktitle = {Category Theory and Computer Science},
 year = {1989}
}

@Book{katz,
  author =       {A. Katz},
  title =        {Principles of Statistical Mechanics: The Information Theoretic Approach},
  publisher =    {WH Freeman},
  year =         1967,
  address =      {San Francisco, CA}
}

@InProceedings{turing,
  author =       {Alan Turing},
  title =        {On Computable Numbers, with an Application to the Entscheidungsproblem},
  booktitle =    {Proceedings of the London Mathematical Society},
  pages =        {230--265},
  year =         1936,
  volume =       42,
  series =       2,
  note =         {Available from: \url{http://www.abelard.org/turpap2/tp2-ie.asp}}
}

@Book{deutsch,
  author =       {David Deutsch},
  title =        {The Fabric of Reality},
  publisher =    {Penguin},
  year =         1997
}

@article{bennett1985fundamental,
  title={The fundamental physical limits of computation},
  author={Bennett, C.H. and Landauer, R.},
  journal={Scientific American},
  volume={253},
  number={1},
  pages={48--56},
  year={1985}
}

@book{walters-cat,
contentTitle = {Frontmatter},
author = {R. F. C. Walters},
title = {Categories and Computer Science},
publisher = {Cambridge University Press},
year = {1992},
url = {http://dx.doi.org/10.1017/CBO9780511608872}
}

@inproceedings{Reed:2010:DMT:1863543.1863568,
 author = {Reed, Jason and Pierce, Benjamin C.},
 title = {Distance makes the types grow stronger: a calculus for differential privacy},
 booktitle = {ICFP},
 year = {2010},
 pages = {157--168},
 numpages = {12},
 publisher = {ACM},
 keywords = {differential privacy, type systems},
}

@INPROCEEDINGS{dwork:differential,
  AUTHOR = "Cynthia Dwork",
  TITLE = "Differential Privacy.",
  booktitle = "ICALP (2)'06",
  PAGES = {1-12},
  YEAR = {2006}
}

@incollection{hatcliff94generic,
    author = "John Hatcliff and Olivier Danvy",
    title = "A Generic Account of Continuation-Passing Styles",
    booktitle = {POPL},
    publisher = {ACM},
    pages = "458--471",
    year = "1994"
}

@inproceedings{Minamide:1996:TCC:237721.237791,
 author = {Minamide, Yasuhiko and Morrisett, Greg and Harper, Robert},
 title = {Typed closure conversion},
 booktitle = {POPL},
 year = {1996},
 pages = {271--283},
 numpages = {13},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@phdthesis{Maslov:2003:RLS:1087512,
 author = {Maslov, Dmitri Aleksandrovich},
 advisor = {Dueck, Gerhard W.},
 title = {Reversible logic synthesis},
 year = {2003},
 isbn = {0-612-98874-0},
 note = {AAINQ98874},
 school = {University of New Brunswick},
 publisher = {University of New Brunswick},
 address = {Fredericton, N.B., Canada, Canada},
}

@Unpublished{petasort,
  author =       {Grzegorz Czajkowski and Mari\'an Dvorsk\'y and Jerry Zhao and Michael Conley},
  title =        {Sorting Petabytes with {MapReduce} - The Next Episode},
  year = 2011,
  note =         {\url{http://googleresearch.blogspot.com/2011/09/sorting-petabytes-with-mapreduce-next.html}}}

@Article{dpa,
  author =       {P. Kocher and J. Jaffe and B. Jun},
  title =        {Differential Power Analysis},
  journal =      {Advances in Cryptology},
  year =         1999}

@Article{burris-lee,
  author =       {S. Burris and S. Lee},
  title =        {Tarski's high school identities},
  journal =      {American Mathematical Monthly},
  year =         1993,
  volume =    100,
  number =    3,
  pages =     {231--236}}

@Article{fiore-remarks,
  author =       {M. P. Fiore and R. {Di Cosmo} and V. Balat},
  title =        {Remarks on Isomorphisms in Typed Calculi with Empty and Sum Types},
  journal =      {Annals of Pure and Applied Logic},
  year =         2006,
  volume =    141,
  number =    {1-2},
  pages =     {35-50}}

@inproceedings{Baez:1997:IN:648335.755726,
 author = {Baez, John C.},
 title = {An Introduction to n-Categories},
 booktitle = {Proceedings of the 7th International Conference on Category Theory and Computer Science},
 series = {CTCS '97},
 year = {1997},
 isbn = {3-540-63455-X},
 pages = {1--33},
 numpages = {33},
 url = {http://dl.acm.org/citation.cfm?id=648335.755726},
 acmid = {755726},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
}

@phdthesis{Riedel:2004:CCC:1048635,
 author = {Riedel, Marc D.},
 advisor = {Bruck, Jehoshua},
 title = {Cyclic combinational circuits},
 year = {2004},
 isbn = {0-496-07100-9},
 note = {AAI3147966},
 publisher = {California Institute of Technology},
 address = {Pasadena, CA, USA},
}

@article{Thapliyal:2010:DRS:1877745.1877748,
 author = {Thapliyal, Himanshu and Ranganathan, Nagarajan},
 title = {Design of reversible sequential circuits optimizing quantum cost, delay, and garbage outputs},
 journal = {J. Emerg. Technol. Comput. Syst.},
 issue_date = {December 2010},
 volume = {6},
 number = {4},
 month = dec,
 year = {2010},
 issn = {1550-4832},
 pages = {14:1--14:31},
 articleno = {14},
 numpages = {31},
 url = {http://doi.acm.org/10.1145/1877745.1877748},
 doi = {10.1145/1877745.1877748},
 acmid = {1877748},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Fredkin gate, Reversible logic, sequential circuits},
}

@article{Selinger:2007:DCC:1229185.1229207,
 author = {Selinger, Peter},
 title = {Dagger Compact Closed Categories and Completely Positive Maps},
 journal = {ENTCS},
 issue_date = {March, 2007},
 volume = {170},
 month = mar,
 year = {2007},
 pages = {139--163},
 numpages = {25},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {CPM construction, Categorical model, dagger categories, quantum computing},
}

@inproceedings{Abramsky:2004:CSQ:1018438.1021878,
 author = {Abramsky, Samson and Coecke, Bob},
 title = {A Categorical Semantics of Quantum Protocols},
 booktitle = {LICS},
 year = {2004}
}

@Article{Landauer,
  author =       {Rolf Landauer},
  title =        {The physical nature of information},
  journal =      {Physics Letters A},
  year =         1996}

@article{citeulike:7374951,
    author = {{Martin-L\"of}, Per},
    journal = {The Journal of Symbolic Logic},
    keywords = {gadt},
    month = mar,
    number = {1},
    pages = {311+},
    title = {{An Intuitionistic Theory of Types: Predicative Part.}},
    volume = {49},
    year = {1984}
}

@PhdThesis{warren,
  author =       {Michael Warren},
  title =        {Homotopy theoretic aspects of constructive type
                  theory},
  school =       {Carnegie-Mellon University},
  year =         2008}

@Unpublished{streicher,
  author =       {Thomas Streicher},
  title =        {Investigations into Intensional Type Theory},
  note =         {Habilitationsschrift, Universit\"at M\"unchen},
  year =      1993}

@inproceedings{Rittri:1989:UTS:99370.99384,
 author = {Rittri, Mikael},
 title = {Using types as search keys in function libraries},
 booktitle = {FPCA},
 year = {1989}
}

@article{Selinger:2011:FDH:1942319.1942398,
 author = {Selinger, Peter},
 title = {Finite Dimensional Hilbert Spaces are Complete for Dagger Compact Closed Categories (Extended Abstract)},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {270},
 number = {1},
 year = {2011},
}

@article{hasegawa2008finite,
  title={Finite dimensional vector spaces are complete for traced symmetric monoidal categories},
  author={Hasegawa, Masahito and Hofmann, Martin and Plotkin, Gordon},
  journal={Pillars of computer science},
  year={2008},
  publisher={Springer}
}

@INPROCEEDINGS{Hofmann96thegroupoid,
    author = {Martin Hofmann and Thomas Streicher},
    title = {The Groupoid Interpretation of Type Theory},
    booktitle = {Venice Festschrift},
    year = {1996},
    pages = {83--111}
}

@Unpublished{danvypage,
  author =       {Olivier Danvy},
  title =        {Home page},
  note =         {\url{http://www.cs.au.dk/~danvy/index-previous.html} accessed October 13, 2013}}

@Unpublished{negative-information,
  author =       {Jonathan Oppenheim and Robert W. Spekkens and Andreas Winter},
  title =        {A classical analogue of negative information},
  note =         {\url{arXiv:quant-ph/0511247}}}

@Unpublished{negative-entropy,
  author =       {L\'idia del Rio and Johan Aberg and Renato Renner and Oscar Dahlsten and Vlatko Vedral},
  title =        {The thermodynamic meaning of negative entropy},
  note =         {\url{arXiv:1009.1630}}}

@Article{groupoidcard,
  author =       {John C. Baez and James Dolan},
  title =        {From finite sets to {Feynman} diagrams},
  journal =      {Mathematics Unlimited - 2001 and beyond, Springer},
  year =         2001,
  volume =    1,
  pages =     {29-50}}

@Unpublished{planardiagrams,
  author =       {A. Joyal and R. Street},
  title =        {Planar diagrams and tensor algebra},
  note =         {\url{http://maths.mq.edu.au/~street/Publications.html}},
  month =     {Sep.},
  year =      1988}

@Article{geometrytensor,
  author =       {A. Joyal and R. Street},
  title =        {The geometry of tensor calculus {I}},
  journal =      {Advances in Mathematics},
  year =         1991,
  volume =    88,
  number =    1,
  pages =     {55-112}}

@Book{hottbook,
  author =    {{The Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{http://homotopytypetheory.org/book}},
  address =   {Institute for Advanced Study},
  year =      2013}

@Article{ringcompletion,
  author =       {Nils Baas and Bj\orn Dundas and Birgit Richter and John Rognes},
  title =        {Ring completion of rig categories},
  journal =      {Journal f\"ur die reine und angewandte Mathematik (Crelles Journal)},
  year =         2012,
  volume =    2013,
  number =    674,
  pages =     {43-80},
  month =     mar}

@Unpublished{neelblog,
  author =       {Neelakantan Krishnaswami},
  title =        {The Geometry of Interaction, as an {OCaml} program},
  note =         {\url{http://semantic-domain.blogspot.com/2012/11/in-this-post-ill-show-how-to-turn.html}},
  year =      2012}

@Article{thomason,
  author =       {R. Thomason},
  title =        {Beware the phony multiplication on {Quillen's} $\mathcal{A}^{-1}\mathcal{A}$},
  journal =      {Proc. Amer. Math. Soc.},
  year =         1980,
  volume =    80,
  number =    4,
  pages =     {569-573}}


@incollection{gcons,
year={1996},
booktitle={CONCUR '96: Concurrency Theory},
volume={1119},
series={Lecture Notes in Computer Science},
title={Retracing some paths in process algebra},
publisher={Springer Berlin Heidelberg},
author={Abramsky, Samson},
pages={1-17}
}

@Book{NC00,
  author =       "M.~Nielsen and I.~Chuang",
  title =        "Quantum Computation and Quantum Information",
  publisher =    "Cambridge University Press",
  address =      "Cambridge",
  year =         "2000"
}

@article{DiCosmo:2005:SSI:1090732.1090734,
 author = {Di Cosmo, Roberto},
 title = {A Short Survey of Isomorphisms of Types},
 journal = {Mathematical. Structures in Comp. Sci.},
 issue_date = {October 2005},
 volume = {15},
 number = {5},
 month = oct,
 year = {2005},
 pages = {825--838},
 numpages = {14},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@article{Fajstrup2006241,
title = "Algebraic topology and concurrency ",
journal = "Theoretical Computer Science ",
volume = "357",
number = "1–3",
pages = "241 - 278",
year = "2006",
note = "Clifford Lectures and the Mathematical Foundations of Programming Semantics ",
issn = "0304-3975",
author = "Lisbeth Fajstrup and Martin Raußen and Eric Goubault",
keywords = "Homotopy",
keywords = "Concurrency",
keywords = "Cubical set",
keywords = "Higher-dimensional automata",
keywords = "Partial order",
keywords = "Partially ordered space "
}

@article {MR2666883,
    AUTHOR = {Kirchner, Florent and Mu{\~n}oz, C{\'e}sar},
     TITLE = {The proof monad},
   JOURNAL = {J. Log. Algebr. Program.},
  FJOURNAL = {The Journal of Logic and Algebraic Programming},
    VOLUME = {79},
      YEAR = {2010},
    NUMBER = {3-5},
     PAGES = {264--277},
      ISSN = {1567-8326},
   MRCLASS = {68T15 (68Q55)},
  MRNUMBER = {2666883},
       DOI = {10.1016/j.jlap.2010.03.002},
       URL = {http://dx.doi.org/10.1016/j.jlap.2010.03.002},
}

@incollection{Gunawardena:2001:HC:377786.377845,
 author = {Gunawardena, Jeremy},
 chapter = {Homotopy and Concurrency},
 title = {Current Trends in Theoretical Computer Science},
 editor = {P\u{a}un, B. and Rozenberg, G. and Salomaa, A.},
 year = {2001},
 isbn = {981-02-4473-8},
 pages = {447--459},
 numpages = {13},
 url = {http://dl.acm.org/citation.cfm?id=377786.377845},
 acmid = {377845},
 publisher = {World Scientific Publishing Co., Inc.},
 address = {River Edge, NJ, USA},
}

@article{Heunen:2015:RMC:2875516.2875606,
 author = {Heunen, Chris and Karvonen, Martti},
 title = {Reversible Monadic Computing},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {December 2015},
 volume = {319},
 number = {C},
 month = dec,
 year = {2015},
 issn = {1571-0661},
 pages = {217--237},
 numpages = {21},
 url = {http://dx.doi.org/10.1016/j.entcs.2015.12.014},
 doi = {10.1016/j.entcs.2015.12.014},
 acmid = {2875606},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Frobenius monad, dagger category, quantum measurement, reversible computing},
}

@InProceedings{quotient,
  author =       {N. Mendler},
  title =        {Quotient types via coequalizers in Martin-L\"of type theory},
  booktitle = {Proceedings of the Logical Frameworks Workshop},
  year =         1990,
  pages =        {349–361}}

@Inbook{Cohen2013,
author="Cohen, Cyril",
chapter="Pragmatic Quotient Types in Coq            ",
title="Interactive Theorem Proving: 4th International Conference, ITP 2013",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="213--228"
}

@Inbook{Carette2016,
author="Carette, Jacques and Sabry, Amr",
chapter="Computing with Semirings and Weak Rig Groupoids",
title="ESOP 2016",
year="2016",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="123--148"
}

@InCollection{laplaza,
  author =       {Laplaza, Miguel L.},
  booktitle =    {Coherence in Categories},
  title =        {Coherence for distributivity},
  series =       {Lecture Notes in Mathematics},
  editor=        {Kelly, G.M. and Laplaza, M. and Lewis, G. and Mac Lane, Saunders},
  publisher =    {Springer Verlag},
  year =         {1972},
  volume =       {281},
  pages =        {29-65},
  doi =          {10.1007/BFb0059555},
  isbn =         {978-3-540-05963-9},
  address =      {Berlin}}

@Unpublished{nlabrig,
  author =       {{nLab}},
  title =        {{rig category}},
  year = {2015},
  note =         {\url{http://ncatlab.org/nlab/show/rig+category}}}

@ARTICLE{2009arXiv0908.4305B,
   author = {{Baez}, J.~C. and {Hoffnung}, A.~E. and {Walker}, C.~D.},
    title = "{Higher-Dimensional Algebra VII: Groupoidification}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {0908.4305},
 primaryClass = "math.QA",
 keywords = {Mathematics - Quantum Algebra, Mathematics - Category Theory, 16G20, 17B37, 20C05, 20L05, 81T18},
     year = 2009,
    month = aug,
   adsurl = {http://adsabs.harvard.edu/abs/2009arXiv0908.4305B},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@Unpublished{groupoidintro,
  author =       {Michael B. Williams},
  title =        {Introduction to Groupoids},
  year = {2016},
  note =         {Available from \url{http://www.math.ucla.edu/~mwilliams/pdf/groupoids.pdf}}}

@Article{ccc,
  author =       {Kelly, G. M. and Laplaza, M. L.},
  title =        {Coherence for Compact Closed Categories},
  journal =      {Journal of Pure and Applied Algebra},
  year =         1980,
  pages =        {193-213}}

@Unpublished{looping,
  author =       {Ernesto Lupercio and Bernado Uribe},
  title =        {Loop Groupoids, Gerbes, and Twisted Sectors on Orbifolds},
  note =         {\url{arXiv:math/0110207} [math.AT]},
  year =      2002}

@book{johnstone2002sketches,
  title={Sketches of an elephant: A topos theory compendium},
  author={Johnstone, Peter T},
  volume={2},
  year={2002},
  publisher={Oxford University Press}
}

@Unpublished{subpullback,
  author =       {Andrej Bauer},
  title =        {Substitution is pullback},
  note =         {\url{http://math.andrej.com/2012/09/28/substitution-is-pullback/}},
  year =      2012}

@book{practicalfoundations,
   title = "Practical foundations of mathematics",
   author = "Taylor, Paul",
   series = "Cambridge studies in advanced mathematics",
   publisher = "Cambridge University Press",
   address = "Cambridge, New York (N. Y.), Melbourne",
   url = "http://opac.inria.fr/record=b1095522",
   isbn = "0-521-63107-6",
   year = 1999
}

@InProceedings{theseus,
  author =       {Roshan P. James and Amr Sabry},
  title =        {Theseus: A High-Level Language for Reversible Computing},
  booktitle = {Work-in-progress report in the Conference on Reversible Computation},
  year =  {2014}}

@proceedings{Field:2012:2103656,
 title = {{POPL '12}: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2012},
 isbn = {978-1-4503-1083-3},
 location = {Philadelphia, PA, USA},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article {vv06,
	title = {A very short note on homotopy $\lambda$-calculus},
	journal = {Unpublished},
	year = {2006},
	month = {September},
	pages = {1{\textendash}7},
	url = {http://www.math.ias.edu/vladimir/files/2006_09_Hlambda.pdf},
	author = {Voevodsky, Vladimir}
}

@book{Hey:1999:FCE:304763,
 editor = {Hey, Anthony J. G.},
 title = {Feynman and Computation: Exploring the Limits of Computers},
 year = {1999},
 isbn = {0-7382-0057-3},
 publisher = {Perseus Books},
 address = {Cambridge, MA, USA},
}

@Unpublished{shulman,
  author =       {Michael Shulman},
  title =        {Categorical logic from a categorical point of view},
  note =         {Draft for AARMS Summer School 2016. Available at \url{http://mikeshulman.github.io/catlog/catlog.pdf}, Version of July 28, 2016}}

@article{buchholtz2017real,
  title={The real projective spaces in homotopy type theory},
  author={Buchholtz, Ulrik and Rijke, Egbert},
  journal={arXiv preprint arXiv:1704.05770},
  year={2017}
}

@article{SimplicialModel,
   author = {{Kapulkin}, C. and {LeFanu Lumsdaine}, P.},
    title = "{The Simplicial Model of Univalent Foundations (after Voevodsky)}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1211.2851},
 primaryClass = "math.LO",
 keywords = {Mathematics - Logic, Mathematics - Algebraic Topology, Mathematics - Category Theory, 03B15, 55U10 (Primary), 18C50, 55U35 (Secondary)},
     year = 2012,
    month = nov,
   adsurl = {http://adsabs.harvard.edu/abs/2012arXiv1211.2851K},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@inproceedings{licata2015cubical,
  title={A cubical approach to synthetic homotopy theory},
  author={Licata, Daniel R and Brunerie, Guillaume},
  booktitle={Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  pages={92--103},
  year={2015},
  organization={IEEE Computer Society}
}

@InProceedings{christensen,
  author =       {Dan Christensen},
  title =        {A characterization of univalent fibrations},
  booktitle = {Category Theory, CT2015},
  year =      2015,
  address =   {Aveiro, Portugal}}