handlers.bib

%https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
@book{mltt,
	author    = {Per Martin-Löf},
	title     = {Intuitionistic Type Theory},
	year      = 1984,
	note      = {Lecture notes by Giovanni Sambin}
}

	% https://www.cs.ox.ac.uk/publications/books/PfS/
@book{prog-from-spec,
	author    = {Caroll Morgan}, 
	title     = {Programming from Specifications},
	publisher = {Prentice Hall},
	year      = 1998,
	edition   = 2
}

	% https://link.springer.com/chapter/10.1007/978-3-319-19797-5_13
@InProceedings{McBride-totally-free,
	author="McBride, Conor",
	editor="Hinze, Ralf
	and Voigtl{\"a}nder, Janis",
	title="Turing-Completeness Totally Free",
	booktitle="Mathematics of Program Construction",
	year="2015",
	publisher="Springer International Publishing",
	address="Cham",
	pages="257--275",
	abstract="In this paper, I show that general recursive definitions can be represented in the free monad which supports the `effect' of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable.",
	isbn="978-3-319-19797-5",
	doi = "10.1007/978-3-319-19797-5_13",
}

	% http://math.andrej.com/wp-content/uploads/2012/03/eff.pdf
@article{eff,
	title = "Programming with algebraic effects and handlers",
	journal = "Journal of Logical and Algebraic Methods in Programming",
	volume = "84",
	number = "1",
	pages = "108 - 123",
	year = "2015",
	note = "Special Issue: The 23rd Nordic Workshop on Programming Theory (NWPT 2011) Special Issue: Domains X, International workshop on Domain Theory and applications, Swansea, 5-7 September, 2011",
	issn = "2352-2208",
	doi = "10.1016/j.jlamp.2014.02.001",
	author = "Andrej Bauer and Matija Pretnar"
}

	% https://www.cs.ox.ac.uk/people/nicolas.wu/papers/Scope.pdf
@inproceedings{effect-handlers-in-scope,
	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},
	pages = {1--12},
	numpages = {12},
	doi = {10.1145/2633357.2633358},
	acmid = {2633358},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {Haskell, effect handlers, modularity, monads, semantics, syntax}
}

	% http://www.staff.science.uu.nl/~swier004/publications/2017-scp.pdf
@article{coq-refinement,
	title = "Embedding the refinement calculus in Coq",
	journal = "Science of Computer Programming",
	volume = "164",
	pages = "37 - 48",
	year = "2018",
	note = "Special issue of selected papers from FLOPS 2016",
	issn = "0167-6423",
	doi = "https://doi.org/10.1016/j.scico.2017.04.003",
	author = "João Alpuim and Wouter Swierstra",
	keywords = "Refinement calculus, Coq, Predicate transformers, Free monad, Dependent types"
}


	% http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf
@phdthesis{agda-thesis,
	title = "Towards a practical programming language based on dependent type theory",
	author = "Ulf Norell",
	institution = "Chalmers University of Technology",
	year = "2007"
}

@online{agda-source-termination,
  shorthand = {Agda2.6},
  title = {agda/Termination.hs},
  author = {{The Agda Team}},
  url = {https://github.com/agda/agda/blob/2a087473e76c96c5767e7b03b0ca403fd99c8173/src/full/Agda/Termination/Termination.hs#L3},
  note = {Agda version 2.6.0.1},
}

@online{lib-mtl,
	title = {mtl: Monad classes, using functional dependencies},
	author = {Gill, Andy and Kmett, Edward},
	url = {http://hackage.haskell.org/package/mtl},
	note = {accessed 22nd Nov 2018}
}

@article{just-do-it,
	author = {Gibbons, Jeremy and Hinze, Ralf},
	title = {Just Do It: Simple Monadic Equational Reasoning},
	journal = {SIGPLAN Not.},
	issue_date = {September 2011},
	volume = {46},
	number = {9},
	month = sep,
	year = {2011},
	issn = {0362-1340},
	pages = {2--14},
	numpages = {13},
	doi = {10.1145/2034574.2034777},
	acmid = {2034777},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {algebraic specification, equational reasoning, lawvere theories, monads}
}

% https://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF
@unpublished{EWD472,
	author = "Edsger W. Dijkstra",
	title = "Guarded commands, non-determinacy and formal derivation of programs",
	month = jan,
	year = "1975",
	note = "published as \cite{EWD:EWD472pub}",
	url = "http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF"
}

@article{EWD:EWD472pub,
	author = "Edsger W. Dijkstra",
	title = "Guarded commands, non-determinacy and formal derivation of programs",
	year = "1975",
	publisher = "ACM",
	journal = "Comm. ACM ",
	volume = 18,
	number = 8,
	pages = {453--457}
}

% Where EWD472 is a set of ideas, this book is the story behind the ideas.
@book{dijkstra-discipline-programming,
	author = {Dijkstra, Edsger Wybe},
	title = {A  Discipline of Programming},
	year = {1976},
	isbn = {013215871X},
	edition = {1st},
	publisher = {Prentice Hall PTR},
	address = {Upper Saddle River, NJ, USA}
}

@article{computation-and-monads,
	title = "Notions of computation and monads",
	journal = "Information and Computation",
	volume = "93",
	number = "1",
	pages = "55 - 92",
	year = "1991",
	note = "Selections from 1989 IEEE Symposium on Logic in Computer Science",
	issn = "0890-5401",
	doi = "https://doi.org/10.1016/0890-5401(91)90052-4",
	author = "Eugenio Moggi"
}

@inproceedings{exceptional-syntax,
	author = {Benton, Nick and Kennedy, Andrew},
	title = {Exceptional Syntax},
	booktitle = {},
	year = {2001},
	month = {07},
	publisher = {CUP},
	url = {https://www.microsoft.com/en-us/research/publication/exceptional-syntax/},
	address = {},
	pages = {395-410},
	journal = {Journal of Functional Programming},
	volume = {11},
	chapter = {}
}

@article{calculating-is-better-than-scheming,
	author = {Wadler, P},
	title = {A Critique of Abelson and Sussman or Why Calculating is Better Than Scheming},
	journal = {SIGPLAN Not.},
	issue_date = {March 1987},
	volume = {22},
	number = {3},
	month = mar,
	year = {1987},
	issn = {0362-1340},
	pages = {83--94},
	numpages = {12},
	doi = {10.1145/24697.24706},
	acmid = {24706},
	publisher = {ACM},
	address = {New York, NY, USA}
}

@inproceedings{monad-transformers,
	author = {Liang, Sheng and Hudak, Paul and Jones, Mark},
	title = {Monad Transformers and Modular Interpreters},
	booktitle = {Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
	series = {POPL '95},
	year = {1995},
	isbn = {0-89791-692-1},
	pages = {333--343},
	numpages = {11},
	doi = {10.1145/199448.199528},
	acmid = {199528},
	publisher = {ACM},
	address = {New York, NY, USA}
}

% predecessor to freer-monads
@inproceedings{extensible-effects,
	author = {Kiselyov, Oleg and Sabry, Amr and Swords, Cameron},
	title = {Extensible Effects: An Alternative to Monad Transformers},
	booktitle = {Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell},
	series = {Haskell '13},
	year = {2013},
	isbn = {978-1-4503-2383-3},
	pages = {59--70},
	numpages = {12},
	doi = {10.1145/2503778.2503791},
	acmid = {2503791},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {coroutine, effect handler, effect interaction, monad, monad transformer, open union, type and effect system}
}

@inproceedings{freer-monads,
	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},
	pages = {94--105},
	numpages = {12},
	doi = {10.1145/2804302.2804319},
	acmid = {2804319},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {Kan extension, coroutine, effect handler, effect interaction, free monad, open union, type and effect system}
}

@article{hoare-axiomatic,
	author = {Hoare, C. A. R.},
	title = {An Axiomatic Basis for Computer Programming},
	journal = {Commun. ACM},
	issue_date = {Oct. 1969},
	volume = {12},
	number = {10},
	month = oct,
	year = {1969},
	issn = {0001-0782},
	pages = {576--580},
	numpages = {5},
	doi = {10.1145/363235.363259},
	acmid = {363259},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {axiomatic method, formal language definition, machine-independent programming, program documentation, programming language design, theory of programming' proofs of programs}
}

@article{troelstra-van-dalen-2,
	number = {2},
	year = {1991},
	title = {Constructivism in Mathematics, Volume 2},
	volume = {50},
	pages = {355--356},
	journal = {Studia Logica},
	publisher = {Springer},
	author = {A. S. Troelstra and D. van Dalen}
}

@online{trouble-type-in-type,
	author = "Liam O'Connor",
	title = "The Trouble with Typing Type as Type",
	year = "2015",
	note = "accessed 3rd Nov 2018",
	url = "http://liamoc.net/posts/2015-09-10-girards-paradox.html"
}

@book{prob-gcl,
	author = {McIver, Annabelle and Morgan, Carroll},
	title = {Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science)},
	year = {2004},
	isbn = {0387401156},
	publisher = {SpringerVerlag},
} 

% https://link.springer.com/content/pdf/10.1007/3-540-45931-6_24.pdf
@inproceedings{notions-to-monad,
  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},
  organization={Springer}
}

@Article{algebraic-operations-and-generic-effects,
author="Plotkin, Gordon
and Power, John",
title="Algebraic Operations and Generic Effects",
journal="Applied Categorical Structures",
year="2003",
month="02",
day="01",
volume="11",
number="1",
pages="69--94",
issn="1572-9095",
doi="10.1023/A:1023064908962",
}

@inproceedings{size-change-termination,
 author = {Lee, Chin Soon and Jones, Neil D. and Ben-Amram, Amir M.},
 title = {The Size-change Principle for Program Termination},
 booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '01},
 year = {2001},
 isbn = {1-58113-336-7},
 pages = {81--92},
 numpages = {12},
 doi = {10.1145/360204.360210},
 acmid = {360210},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {PSPACE-completeness, omega automaton, partial evaluation, program analysis, termination},
} 

@article{formalization-properties-functional-programs,
 author = {Manna, Zohar and Pnueli, Amir},
 title = {Formalization of Properties of Functional Programs},
 journal = {J. ACM},
 issue_date = {July 1970},
 volume = {17},
 number = {3},
 month = jul,
 year = {1970},
 issn = {0004-5411},
 pages = {555--569},
 numpages = {15},
 doi = {10.1145/321592.321606},
 acmid = {321606},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@conference{bananas-lenses-envelopes-and-barbed-wire,
title = "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire",
abstract = "We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's {"}Introduction to Functional Programming{"} can be expressed using these operators.",
keywords = "EWI-7281, IR-56289",
author = "Erik Meijer and J. Hughes and M.M. Fokkinga and Ross Paterson",
year = "1991",
month = "8",
doi = "10.1007/3540543961_7",
pages = "124--144",
}

@inproceedings{sigbovik-portmantout,
  title = {The Portmantout},
  author = {Murphy, VII Ph.D., Dr. Tom},
  booktitle = {A Record of the Proceedings of SIGBOVIK 2015},
  series = {SIGBOVIK},
  year = {2015},
  month = {04},
  day = {01},
  issn = {2155-0166},
  pages = {85--98},
}

@inproceedings{sigbovik-shortmantout,
  title = {A Shortmantout},
  author = {David Renshaw and Jim McCann},
  booktitle = {A Record of the Proceedings of SIGBOVIK 2016},
  series = {SIGBOVIK},
  year = {2016},
  month = {04},
  day = {01},
  issn = {2155-0166},
  pages = {0x4ccd69669eb3ec09434da6ad0e127cfc7b86169bf24a3fb135042d60e3ec1fdf--0x88d34007416e70009614ed5ee1bc590881f346feebcbc122d93004be50449be1},
}

@inproceedings{sigbovik-optimal-portmantout,
  title = {Efficient Computation of an Optimal Portmantout},
  author = {David Renshaw},
  booktitle = {A Record of the Proceedings of SIGBOVIK 2017},
  series = {SIGBOVIK},
  year = {2017},
  month = {04},
  day = {00},
  issn = {2155-0166},
  pages = {176--189},
}

@inproceedings{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}
}

@article{on-computable-numbers,
    author = {Turing, A. M.},
    title = "{On Computable Numbers, with an Application to the Entscheidungsproblem}",
    journal = {Proceedings of the London Mathematical Society},
    volume = {s2-42},
    number = {1},
    pages = {230-265},
    year = {1937},
    month = {01},
    issn = {0024-6115},
    doi = {10.1112/plms/s2-42.1.230},
    eprint = {http://oup.prod.sis.lan/plms/article-pdf/s2-42/1/230/4317544/s2-42-1-230.pdf},
}

@inproceedings{pt-semantics-for-effects,
  title = "A predicate transformer semantics for effects (Functional Pearl)",
  author = {Wouter Swierstra and Tim Baanen},
  booktitle = {Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming},
  series = {ICFP '19},
  year = {2019},
  articleno = {103},
  doi = {10.1145/3341707},
}

@book {categories-for-working-mathematician,
    AUTHOR = {MacLane, Saunders},
     TITLE = {Categories for the working mathematician},
      NOTE = {Graduate Texts in Mathematics, Vol. 5},
 PUBLISHER = {Springer-Verlag, New York-Berlin},
      YEAR = {1971},
     PAGES = {ix+262},
}

@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}
}
@incollection{aczel-acc,
  title = "An Introduction to Inductive Definitions",
  editor = "Jon Barwise",
  series = "Studies in Logic and the Foundations of Mathematics",
  publisher = "Elsevier",
  volume = "90",
  pages = "739 - 782",
  year = "1977",
  booktitle = "Handbook of Mathematical Logic",
  issn = "0049-237X",
  doi = "https://doi.org/10.1016/S0049-237X(08)71120-0",
  author = "Peter Aczel",
}
@book{dragon-book,
 author = {Aho, Alfred and Ullman, Jeffrey D.},
 title = {Principles of compiler design},
 publisher = {Addison-Wesley Pub. Co},
 year = {1977},
 address = {Reading, Mass},
 isbn = {0201000229},
}
@article{Brzozowski,
 author = {Brzozowski, Janusz A.},
 title = {Derivatives of Regular Expressions},
 journal = {JACM},
 issue_date = {Oct. 1964},
 volume = 11,
 number = 4,
 month = oct,
 year = 1964,
 issn = {0004-5411},
 pages = {481--494},
 numpages = 14,
 doi = {10.1145/321239.321249},
 acmid = 321249,
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@inproceedings{dependent-grammar,
  author = {Kasper Brink and Stefan Holdermans and Andres Löh},
  title = {Dependently Typed Grammars},
  year = {2010},
  month = {06},
  pages = {58-79},
  doi = {10.1007/978-3-642-13321-3_6}
}

@unpublished{coinductive-trie,
  author = {Andreas Abel},
  title = {Equational Reasoning about Formal Languages in Coalgebraic Style},
  year = {2016},
  month = {12},
  day = {23},
  note={preprint available at \url{http://www.cse.chalmers.se/~abela/jlamp17.pdf}},
}

@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}
}

@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{dijkstra-monads-for-free,
 author = {Ahman, Danel and Hriundefinedcu, Cundefinedtundefinedlin 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},
 year = {2017},
 isbn = {9781450346603},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 doi = {10.1145/3009837.3009878},
 booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 pages = {515–529},
 numpages = {15},
 keywords = {proof assistants, dependent types, effectful programming, verification},
 series = {POPL 2017}
}

@article{dijkstra-monads-for-all,
 author = {Maillard, Kenji and Ahman, Danel and Atkey, Robert and Mart\'{\i}nez, Guido and Hriundefinedcu, Cundefinedtundefinedlin and Rivas, Exequiel and Tanter, \'{E}ric},
 title = {Dijkstra Monads for All},
 year = {2019},
 issue_date = {July 2019},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 volume = {3},
 number = {ICFP},
 doi = {10.1145/3341708},
 journal = {Proc. ACM Program. Lang.},
 month = jul,
 articleno = {Article 104},
 numpages = {29},
 keywords = {program verification, dependent types, foundations, side-effects, monads}
}


@book{standard-ml,
  title={The Definition of Standard ML},
  author={Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
  publisher={The MIT Press},
  year={1997}
}

@article{harper-regex,
  title={Proof-directed debugging},
  volume={9},
  DOI={10.1017/S0956796899003378},
  number={4},
  journal={Journal of Functional Programming},
  publisher={Cambridge University Press},
  author={Robert Harper},
  year={1999},
  pages={463–469}
}

@article{hutton,
  title={Higher-order functions for parsing},
  volume={2},
  DOI={10.1017/S0956796800000411},
  number={3},
  journal={Journal of Functional Programming},
  publisher={Cambridge University Press},
  author={Hutton, Graham},
  year={1992},
  pages={323–343}
}

@inproceedings{swierstra-duponcheel,
	author = {S. Doaitse Swierstra and Luc Duponcheel},
	title = {Deterministic, Error-Correcting Combinator Parsers},
	booktitle = {Advanced Functional Programming},
	year = {1996},
	pages = {184--207},
	publisher = {Springer-Verlag},
	doi = {10.1007/3-540-61628-4_7},
}

@inproceedings{list-of-successes,
 author = {Wadler, Philip},
 title = {How to Replace Failure by a List of Successes},
 booktitle = {Proc. Of a Conference on Functional Programming Languages and Computer Architecture},
 year = {1985},
 pages = {113--128},
 numpages = {16},
 doi = {10.1007/3-540-15975-4_33},
 acmid = {5288},
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},
} 

@article{total-parser-combinators,
 author = {Danielsson, Nils Anders},
 title = {Total Parser Combinators},
 journal = {SIGPLAN Not.},
 issue_date = {September 2010},
 volume = {45},
 number = {9},
 month = sep,
 year = {2010},
 issn = {0362-1340},
 pages = {285--296},
 numpages = {12},
 doi = {10.1145/1932681.1863585},
 acmid = {1863585},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {dependent types, mixed induction and coinduction, parser combinators, productivity, termination},
} 

@phdthesis{firsov-certification-context-free-grammars,
  title = {Certification of Context-Free Grammar Algorithms},
  author = {Firsov, Denis},
  institution = {Institute of Cybernetics at Tallinn University of Technology },
  year = {2016}
}

@inproceedings{categories-of-containers,
    author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
    title = {Categories of Containers},
    booktitle = {Proceedings of Foundations of Software Science and Computation Structures},
    year = {2003},
	doi = {10.1007/3-540-36576-1_2}
}

@article{ooagda,
	author = {Abel, Andreas and Adelsberger, Stephan and Setzer, Anton},
	year = {2017},
	month = {02},
	pages = {},
	title = {Interactive programming in Agda – Objects and graphical user interfaces},
	volume = {27},
	journal = {Journal of Functional Programming},
	doi = {10.1017/S0956796816000319}
}


@article{la-carte, 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}}

@unpublished{intrinsic-verification-regex,
	title={Intrinsic Verification of a Regular Expression Matcher},
	author={Korkut, Joomy and Trifunovski, Maksim and Licata, Daniel R.},
	year = {2016},
	month = {1},
	day = {15},
	note = {preprint available at \url{http://dlicata.web.wesleyan.edu/pubs/ktl16regexp/ktl16regexp.pdf}},
}

@InProceedings{simple-functional-cfg-parsing,
author="Ridge, Tom",
editor="Jouannaud, Jean-Pierre
and Shao, Zhong",
title="Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars",
booktitle="Certified Programs and Proofs",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="103--118",
abstract="Parsers for context-free grammars can be implemented directly and naturally in a functional style known as ``combinator parsing'', using recursion following the structure of the grammar rules. However, naive implementations fail to terminate on left-recursive grammars, and despite extensive research the only complete parsers for general context-free grammars are constructed using other techniques such as Earley parsing. Our main contribution is to show how to construct simple, sound and complete parser implementations directly from grammar specifications, for all context-free grammars, based on combinator parsing. We then construct a generic parser generator and show that generated parsers are sound and complete. The formal proofs are mechanized using the HOL4 theorem prover. Memoized parsers based on our approach are polynomial-time in the size of the input. Preliminary real-world performance testing on highly ambiguous grammars indicates our parsers are faster than those generated by the popular Happy parser generator.",
isbn="978-3-642-25379-9",
doi = {10.1007/978-3-642-25379-9_10},
}

@inproceedings{functional-parsers,
 author = {Fokker, Jeroen},
 title = {Functional Parsers},
 year = {1995},
 isbn = {3540594515},
 publisher = {Springer},
 address = {Berlin, Heidelberg},
 booktitle = {Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text},
 pages = {1–23},
 numpages = {23},
 doi = {10.1007/3-540-59451-5_1},
}

@techreport{leijen2001parsec,
  title={Parsec: Direct style monadic parser combinators for the real world},
  author={Leijen, Daan and Meijer, Erik},
  year={2001},
  edition = {Technical Report UU-CS-2001-35, Departement of Computer Science, Universiteit Utrecht},
  number = {UU-CS-2001-27},
}

@inproceedings{efficient-combinator-parsers,
 author = {Koopman, Pieter W. M. and Plasmeijer, Marinus J.},
 title = {Efficient Combinator Parsers},
 year = {1998},
 isbn = {3540662294},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 booktitle = {Selected Papers from the 10th International Workshop on 10th International Workshop},
 pages = {120–136},
 numpages = {17},
 series = {IFL ’98},
 doi = {10.1007/3-540-48515-5_8},
}

@inproceedings{parsing-with-derivatives,
 author = {Might, Matthew and Darais, David and Spiewak, Daniel},
 title = {Parsing with Derivatives: A Functional Pearl},
 year = {2011},
 isbn = {9781450308656},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 doi = {10.1145/2034773.2034801},
 booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},
 pages = {189–195},
 numpages = {7},
 keywords = {parser combinator, context-free grammar, parsing, derivative, formal languages, regular expressions},
 series = {ICFP ’11}
}

@inproceedings{parser-combinators-for-left-recursive,
 author = {Frost, Richard A. and Hafiz, Rahmatullah and Callaghan, Paul},
 title = {Parser Combinators for Ambiguous Left-Recursive Grammars},
 year = {2008},
 isbn = {3540774416},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 booktitle = {Proceedings of the 10th International Conference on Practical Aspects of Declarative Languages},
 pages = {167–181},
 numpages = {15},
 keywords = {left recursion, functional programming, parser combinators, natural-language parsing, ambiguity},
 series = {PADL’08},
 doi = {10.1007/978-3-540-77442-6_12},
}

@inproceedings{instance-arguments-agda,
 author = {Devriese, Dominique and Piessens, Frank},
 title = {On the Bright Side of Type Classes: Instance Arguments in Agda},
 year = {2011},
 isbn = {9781450308656},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 doi = {10.1145/2034773.2034796},
 booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},
 pages = {143–155},
 numpages = {13},
 keywords = {agda, type classes, ad hoc polymorphism, instance arguments},
 series = {ICFP ’11}
}

@inproceedings{algebraic-effect-handlers,
 author = {Plotkin, Gordon and Pretnar, Matija},
 title = {Handlers of Algebraic Effects},
 year = {2009},
 isbn = {9783642005893},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 doi = {10.1007/978-3-642-00590-9_7},
 booktitle = {Proceedings of the 18th European Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009},
 pages = {80–94},
 numpages = {15},
 series = {ESOP ’09}
}


@inproceedings{modular-algebraic-effects,
 author = {Schrijvers, Tom and Pir\'{o}g, Maciej and Wu, Nicolas and Jaskelioff, Mauro},
 title = {Monad Transformers and Modular Algebraic Effects: What Binds Them Together},
 year = {2019},
 isbn = {9781450368131},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 doi = {10.1145/3331545.3342595},
 booktitle = {Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell},
 pages = {98–113},
 numpages = {16},
 keywords = {Transformers, Monads, Handlers, Effects},
 series = {Haskell 2019}
}

@article{effects-and-monads,
author = {Wadler, Philip and Thiemann, Peter},
title = {The Marriage of Effects and Monads},
year = {2003},
issue_date = {January 2003},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {1},
issn = {1529-3785},
doi = {10.1145/601775.601776},
journal = {ACM Trans. Comput. Logic},
month = jan,
pages = {1–32},
numpages = {32},
keywords = {effect, region, type, type reconstruction, Monad}
}


@inproceedings{embedding-effect-systems,
author = {Orchard, Dominic and Petricek, Tomas},
title = {Embedding Effect Systems in Haskell},
year = {2014},
isbn = {9781450330411},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/2633357.2633368},
booktitle = {Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell},
pages = {13–24},
numpages = {12},
keywords = {parametric effect monads, effect systems, type systems},
series = {Haskell ’14}
}