handlers.bib

@inproceedings{Gibbons:2011:JSM:2034773.2034777,
 author = {Gibbons, Jeremy and Hinze, Ralf},
 title = {Just Do It: Simple Monadic Equational Reasoning},
 booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '11},
 year = {2011},
 isbn = {978-1-4503-0865-6},
 location = {Tokyo, Japan},
 pages = {2--14},
 url = {http://doi.acm.org/10.1145/2034773.2034777},
 doi = {10.1145/2034773.2034777},
 acmid = {2034777},
 publisher = {ACM},
 keywords = {algebraic specification, equational reasoning, lawvere theories, monads},
} 

@PhdThesis{agda,
  author =       {Ulf Norell},
  title =        {Towards a practical programming language based on dependent type theory},
  school =       {Chalmers University of Technology},
  year =         {2007},
}

@inproceedings{hancock-setzer-II,
  title={Specifying interactions with dependent types},
  author={Hancock, Peter and Setzer, Anton},
  booktitle={Workshop on Subtyping and Dependent Types in Programming},
  publisher={INRIA},
  numpages=13,
  articleno=5,
  address={Ponte de Lima, Portugal},
  year=2000,
  editors={Gilles Barthe and Peter Dybjer}
}

@inproceedings{hancock-setzer-I,
author="Hancock, Peter and Setzer, Anton",
editor="Clote, Peter G. and Schwichtenberg, Helmut",
title="Interactive Programs in Dependent Type Theory",
bookTitle="Computer Science Logic: 14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 -- 26, 2000 Proceedings",
year="2000",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="317--331",
isbn="978-3-540-44622-4",
doi="10.1007/3-540-44622-2_21",
url="https://doi.org/10.1007/3-540-44622-2_21"
}

@article{wadler-critique,
  title={A critique of Abelson and Sussman or why calculating is better than scheming},
  author={Wadler, Philip},
  journal={ACM SIGPLAN Notices},
  volume={22},
  number={3},
  pages={83--94},
  year={1987},
  publisher={ACM}
}


@Book{algebra-of-programming,
  author =    {Richard Bird and Oege {\tussenvoegsel{De}{de} Moor}},
  shortauthor = {Bird and De Moor},
  title =        {The algebra of programming},
  publisher =    {Prentice Hall},
  year =         {1996}
}

@book{pearls,
  author =    {Richard Bird},
  title =        {Pearls of Functional Algorithm Design},
  publisher =    {Cambridge University Press},
  year =         {2010}
}

@manual{coq,
  author = {{Coq} {Development} {Team}, The},
  title  = {The {Coq} Proof Assistant Reference Manual, version 8.7},
  month  = Oct,
  organization = {ADT Coq (Action for Technological Development)},
  year   = {2017},
  url    = {http://coq.inria.fr}
}

@article{brady,
  title={Idris, a general-purpose dependently typed programming language: Design and implementation},
  author={Brady, Edwin},
  journal={Journal of Functional Programming},
  volume={23},
  number={5},
  pages={552--593},
  year={2013},
  publisher={Cambridge University Press}
}

@book{morgan1994programming,
  title={Programming from specifications},
  author={Morgan, Carroll},
  year={1994},
  publisher={Prentice Hall,}
}

@book{back2012refinement,
  title={Refinement calculus: a systematic introduction},
  author={Back, Ralph-Johan and {von Wright}, Joakim},
  year=2012,
  publisher={Springer Graduate Texts in Computer Science}
}

@Article{gcl,
  author =       {Edsger W.~Dijkstra},
  title =        {Guarded commands, non-determinacy and formal. derivation of programs},
  journal =      {Communications of the ACM},
  year =         {1975},
  volume =    {18},
  number =    {8},
  pages =     {453-457}
}

@inproceedings{plotkin2002notions,
  title={Notions of computation determine monads},
  author={Plotkin, Gordon and Power, John},
  booktitle={International Conference on Foundations of Software Science and Computation Structures},
  pages={342--356},
  year={2002},
  publisher={Springer}
}

@phdthesis{pretnar2010logic,
  title={Logic and handling of algebraic effects},
  author={Pretnar, Matija},
  year={2010},
  school={The University of Edinburgh}
}

@unpublished{hutton2008reasoning,
  title={Reasoning about effects: Seeing the wood through the trees},
  author={Hutton, Graham and Fulger, Diana},
  booktitle={Proceedings of the Ninth Symposium on Trends in Functional Programming},
  year={2008}
}

@inproceedings{mcbride2015turing,
  title={Turing-completeness totally free},
  author={McBride, Conor},
  booktitle={International Conference on Mathematics of Program Construction},
  pages={257--275},
  year={2015},
  publisher={Springer}
}

@article{bove_krauss_sozeau_2016, title={Partiality and recursion in interactive theorem provers – an overview}, volume={26}, DOI={10.1017/S0960129514000115}, number={1}, journal={Mathematical Structures in Computer Science}, publisher={Cambridge University Press}, author={Bove, Ana and Krauss, Alexander and Sozeau, Matthieu}, year={2016}, pages={38–88}}


@book{osullivan2008real,
  title={Real world haskell: Code you can believe in},
  author={O'Sullivan, Bryan and Goerzen, John and Stewart, Donald Bruce},
  year={2008},
  publisher={" O'Reilly Media, Inc."}
}

@article{swierstra2008, title={Data types à la carte}, volume={18},
                  DOI={10.1017/S0956796808006758}, number={4},
                  journal={Journal of Functional Programming},
                  publisher={Cambridge University Press},
                  author={Swierstra, Wouter}, year={2008},
                  pages={423–436}}

@article{indexed,
  title={Indexed containers},
  author={Altenkirch, Thorsten and Ghani, Neil and Hancock, Peter and McBride, Conor and Morris, Peter},
  journal={Journal of Functional Programming},
  volume={25},
  year={2015},
  doi={10.1017/S095679681500009X},
  publisher={Cambridge University Press}
}

@article{bove-capretta,
  title={Modelling general recursion in type theory},
  author={Bove, Ana and Capretta, Venanzio},
  journal={Mathematical Structures in Computer Science},
  volume={15},
  number={4},
  pages={671--708},
  year={2005},
  publisher={Cambridge University Press}
}

@article{capretta,
  title     = {General Recursion via Coinductive Types},
  author={Capretta, Venanzio},
  journal={Logical Methods in Computer Science},
  volume={1},
  number={2},
  pages={1--28},
  year={2005}
}


@inproceedings{dijkstra-monad,
 author = {Swamy, Nikhil and Weinberger, Joel and Schlesinger, Cole and Chen, Juan and Livshits, Benjamin},
 title = {Verifying Higher-order Programs with the Dijkstra Monad},
 booktitle = {Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '13},
 year = {2013},
 isbn = {978-1-4503-2014-6},
 location = {Seattle, Washington, USA},
 pages = {387--398},
 doi = {10.1145/2491956.2491978},
 acmid = {2491978},
 publisher = {ACM},
 keywords = {dynamic languages, hoare monad, predicate transformer, refinement types},
} 


@inproceedings{fstar,
  author    = {Nikhil Swamy and
               Juan Chen and
               C{\'{e}}dric Fournet and
               Pierre{-}Yves Strub and
               Karthikeyan Bhargavan and
               Jean Yang},
  title     = {Secure distributed programming with value-dependent types},
  booktitle = {Proceeding of the 16th {ACM} {SIGPLAN} {International Conference} on
               {Functional Programming}},
  shortbooktitle = {ICFP},
  pages     = {266--278},
  year      = {2011},
  ee        = {http://doi.acm.org/10.1145/2034773.2034811},
  doi       = {10.1145/2034773.2034811},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/SwamyCFSBY11},
  editor    = {Manuel M. T. Chakravarty and
               Zhenjiang Hu and
               Olivier Danvy},
  publisher = {{ACM}},
  isbn      = {978-1-4503-0865-6}
}


BibTeX | EndNote | ACM Ref

@inproceedings{beauty,
 author = {Swierstra, Wouter and Altenkirch, Thorsten},
 title = {Beauty in the Beast: a functional semantics for the awkward squad},
 booktitle = {Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop},
 series = {Haskell '07},
 year = {2007},
 isbn = {978-1-59593-674-5},
 location = {Freiburg, Germany},
 pages = {25--36},
 url = {http://doi.acm.org/10.1145/1291201.1291206},
 doi = {10.1145/1291201.1291206},
 acmid = {1291206},
 publisher = {ACM},
} 


@phdthesis{swierstra-phd,
  title={A functional specification of effects},
  author={Swierstra, Wouter},
  year={2009},
  school={University of Nottingham}
}



@inproceedings{voigtlaender:free-monads,
	Author = {Janis Voigtl\"ander},
	Booktitle = {Mathematics of Program Construction, Marseille, France,              Proceedings},
	Date-Added = {2008-09-06 13:41:28 +0100},
	Date-Modified = {2008-09-06 13:41:51 +0100},
	Editor = {Christine Paulin-Mohring and Philippe Audebaud},
	Month = JUL,
	Pages = {388-403},
	Publisher = {Springer-Verlag},
	Series = {LNCS},
	Title = {Asymptotic Improvement of Computations over Free Monads},
	Volume = 5133,
	Year = 2008}



@inproceedings{nanevski3,
 author = {Nanevski, Aleksandar and Morrisett, Greg and Shinnar, Avraham and Govereau, Paul and Birkedal, Lars},
 title = {Ynot: Dependent Types for Imperative Programs},
 booktitle = {Proceedings of the 13th {ACM SIGPLAN International Conference on Functional Programming}},
 series = {ICFP '08},
 year = {2008},
 isbn = {978-1-59593-919-7},
 location = {Victoria, BC, Canada},
 pages = {229--240},
 url = {http://doi.acm.org/10.1145/1411204.1411237},
 doi = {10.1145/1411204.1411237},
 acmid = {1411237},
 publisher = {ACM},
 keywords = {Hoare logic, monads, separation logic, type theory},
} 

@InProceedings{hoare-wouter,
author="Swierstra, Wouter",
editor="Berghofer, Stefan
and Nipkow, Tobias
and Urban, Christian
and Wenzel, Makarius",
title="A {Hoare} Logic for the State Monad",
booktitle="Theorem Proving in Higher Order Logics",
year="2009",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="440--451",
isbn="978-3-642-03359-9"
}



@inproceedings{liang-hudak-jones:transformers,
	Author = {Sheng Liang and Paul Hudak and Mark Jones},
	Booktitle = {Conference record of the 22nd {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
	Date-Added = {2007-10-17 13:46:00 +0100},
	Date-Modified = {2007-10-17 13:46:00 +0100},
	Pages = {333--343},
        publisher = {ACM},
	Title = {Monad transformers and modular interpreters},
	Year = {1995}}

 [download]

@inproceedings{nanevski2,
 author = {Nanevski, Aleksandar and Morrisett, Greg and Birkedal, Lars},
 title = {Polymorphism and Separation in Hoare Type Theory},
 booktitle = {Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '06},
 year = {2006},
 isbn = {1-59593-309-3},
 location = {Portland, Oregon, USA},
 pages = {62--73},
 url = {http://doi.acm.org/10.1145/1159803.1159812},
 doi = {10.1145/1159803.1159812},
 acmid = {1159812},
 publisher = {ACM},
 keywords = {hoare logic, separation logic, type theory},
} 


@techreport{nanevski1,
	Author = {Aleksandar Nanevski and Greg Morrisett},
	Date-Added = {2007-10-17 13:46:00 +0100},
	Date-Modified = {2007-10-17 13:46:00 +0100},
	Institution = {Harvard University},
	Number = {TR-24-05},
	Title = {Dependent Type Theory of Stateful Higher-Order Functions},
	Year = {2005}}
@inproceedings{alpuim1,
  author    = {Wouter Swierstra and
               Jo{\~{a}}o Alpuim},
  title     = {From Proposition to Program - Embedding the Refinement Calculus in
               Coq},
  booktitle = {Functional and Logic Programming - 13th International Symposium, {FLOPS}
               2016, Kochi, Japan, March 4-6, 2016, Proceedings},
  pages     = {29--44},
  year      = {2016},
  publisher = {Springer},
  series    = {LNCS},
  volume    =  9613,
  url       = {https://doi.org/10.1007/978-3-319-29604-3\_3},
  doi       = {10.1007/978-3-319-29604-3\_3},
  timestamp = {Sun, 21 May 2017 00:19:14 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/flops/SwierstraA16}

}

@article{alpuim2,
  title={Embedding the refinement calculus in Coq},
  author={Alpuim, Jo{\~{a}}o and Swierstra, Wouter},
  journal={Science of Computer Programming},
  volume={164},
  pages={37--48},
  year={2018},
  publisher={Elsevier}
}

@InProceedings{gibbons,
author="Gibbons, Jeremy",
editor="Wolff, Burkhart
and Gaudel, Marie-Claude
and Feliachi, Abderrahmane",
title="Unifying Theories of Programming with Monads",
booktitle="Unifying Theories of Programming",
year="2013",
publisher="Springer",
pages="23--67",
isbn="978-3-642-35705-3"
}



@inproceedings{gibbons-hinze,
 author = {Gibbons, Jeremy and Hinze, Ralf},
 title = {Just Do It: Simple Monadic Equational Reasoning},
 booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '11},
 year = {2011},
 isbn = {978-1-4503-0865-6},
 location = {Tokyo, Japan},
 pages = {2--14},
 url = {http://doi.acm.org/10.1145/2034773.2034777},
 doi = {10.1145/2034773.2034777},
 acmid = {2034777},
 publisher = {ACM}
} 



@ARTICLE{old-hol,
    author = {R. J. R. Back and J. von Wright},
    title = {Refinement Concepts Formalized in Higher Order Logic},
    journal = {Formal Aspects of Computing},
    year = {1989},
    volume = {2}
}

@inproceedings{butler,
       booktitle = {Proc. Conf. Formal Methods Pacific'97, Springer Series in Discrete Mathematics and Theoretical Computer Science},
          editor = {L. Groves and S. Reeves},
           title = {The Refinement Calculator: Proof Support for Program Refinement},
          author = {M. J. Butler and J. Grundy and T. L{\r a}ngbacka and R. Ruksenas and J. von Wright},
            year = {1997},
           pages = {40--61},
}


@inproceedings{dongol,
year={2015},
booktitle={Mathematics of Program Construction},
volume={9129},
series={LNCS},
title={A Program Construction and Verification Tool for Separation Logic},
author={Dongol, Brijesh and Gomes, Victor B.F. and Struth, Georg},
pages="137--158",
publisher={Springer}
}

@inproceedings{boulme,
  title={Intuitionistic refinement calculus},
  author={Boulm{\'e}, Sylvain},
  booktitle={Typed Lambda Calculi and Applications},
  pages={54--69},
  publisher={Springer},
  year={2007}
}

 [download]

@inproceedings{Wu2014,
 author = {Wu, Nicolas and Schrijvers, Tom and Hinze, Ralf},
 title = {Effect Handlers in Scope},
 booktitle = {Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell},
 series = {Haskell '14},
 year = {2014},
 isbn = {978-1-4503-3041-1},
 location = {Gothenburg, Sweden},
 pages = {1--12},
 url = {http://doi.acm.org/10.1145/2633357.2633358},
 doi = {10.1145/2633357.2633358},
 acmid = {2633358},
 publisher = {ACM},
 keywords = {Haskell, effect handlers, modularity, monads, semantics, syntax},
} 


@inproceedings{brady-effects,
 author = {Brady, Edwin},
 title = {Programming and Reasoning with Algebraic Effects and Dependent Types},
 booktitle = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '13},
 year = {2013},
 isbn = {978-1-4503-2326-0},
 location = {Boston, Massachusetts, USA},
 pages = {133--144},
 url = {http://doi.acm.org/10.1145/2500365.2500581},
 doi = {10.1145/2500365.2500581},
 acmid = {2500581},
 publisher = {ACM}
}
@InProceedings{janis,
author="Voigtl{\"a}nder, Janis",
editor="Audebaud, Philippe
and Paulin-Mohring, Christine",
title="Asymptotic Improvement of Computations over Free Monads",
booktitle="Mathematics of Program Construction",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="388--403",
isbn="978-3-540-70594-9"
}

@inproceedings{freer,
 author = {Kiselyov, Oleg and Ishii, Hiromi},
 title = {Freer Monads, More Extensible Effects},
 booktitle = {Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell},
 series = {Haskell '15},
 year = 2015,
 isbn = {978-1-4503-3808-0},
 location = {Vancouver, BC, Canada},
 pages = {94--105},
 url = {http://doi.acm.org/10.1145/2804302.2804319},
 doi = {10.1145/2804302.2804319},
 acmid = 2804319,
 publisher = {ACM}
} 

@inproceedings{snapl,
  title={The end of history? Using a proof assistant to replace language design with library design},
  author={Chlipala, Adam and Delaware, Benjamin and Duchovni, Samuel and Gross, Jason and Pit-Claudel, Cl{\'e}ment and Suriyakarn, Sorawit and Wang, Peng and Ye, Katherine},
  booktitle={2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  year={2017},
  publisher={Schloss Dagstuhl-Leibniz-Zentrum f\"ur Informatik}
}

@article{plotkin-power-2003,
  title={Algebraic operations and generic effects},
  author={Plotkin, Gordon and Power, John},
  journal={Applied categorical structures},
  volume={11},
  number={1},
  pages={69--94},
  year={2003},
  publisher={Springer}
}

@article{tensor,
  title={Combining effects: Sum and tensor},
  author={Hyland, Martin and Plotkin, Gordon and Power, John},
  journal={Theoretical Computer Science},
  volume={357},
  number={1-3},
  pages={70--99},
  year={2006},
  publisher={Elsevier}
}

@inproceedings{ordered,
  title={Preorders on monads and coalgebraic simulations},
  author={Katsumata, Shin-ya and Sato, Tetsuya},
  booktitle={International Conference on Foundations of Software Science and Computational Structures},
  pages={145--160},
  year={2013},
  organization={Springer}
}

@article{ahman2017handling,
  title={Handling fibred algebraic effects},
  author={Ahman, Danel},
  journal={Proceedings of the ACM on Programming Languages},
  volume={2},
  number={POPL},
  pages={7},
  year={2017},
  publisher={ACM}
}

 BibTeX | EndNote | ACM Ref

@inproceedings{dijkstra-free,
 author = {Ahman, Danel and Hri\c{t}cu, C\u{a}t\u{a}lin and Maillard, Kenji and Mart\'{\i}nez, Guido and Plotkin, Gordon and Protzenko, Jonathan and Rastogi, Aseem and Swamy, Nikhil},
 title = {Dijkstra Monads for Free},
 booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series = {POPL 2017},
 year = {2017},
 isbn = {978-1-4503-4660-3},
 location = {Paris, France},
 pages = {515--529},
 numpages = {15},
 doi = {10.1145/3009837.3009878},
 acmid = {3009878},
 publisher = {ACM}
} 

 [download]

@inproceedings{multi-monadic,
 author = {Swamy, Nikhil and Hri\c{t}cu, C\u{a}t\u{a}lin and Keller, Chantal and Rastogi, Aseem and Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, C{\'e}dric and Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-B{\'e}guelin, Santiago},
 title = {Dependent Types and Multi-monadic Effects in F*},
 booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '16},
 year = {2016},
 isbn = {978-1-4503-3549-2},
 location = {St. Petersburg, FL, USA},
 pages = {256--270},
 numpages = {15},
 url = {http://doi.acm.org/10.1145/2837614.2837655},
 doi = {10.1145/2837614.2837655},
 acmid = {2837655},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {effectful programming, proof assistants, verification},
} 

@misc{maillard,
    title={Dijkstra Monads for All},
    author={Kenji Maillard and Danel Ahman and Robert Atkey and Guido Martinez and Catalin Hritcu and Exequiel Rivas and Éric Tanter},
    year={2019},
    eprint={1903.01237},
    archivePrefix={arXiv},
    primaryClass={cs.PL}
}