@string{IPL="Information Processing Letters"}
@string{Springer="Springer"}
@string{LNCS="LNCS"}

@inproceedings{BerghoferN-TYPES00,author={Stefan Berghofer and Tobias Nipkow},
title={Executing Higher Order Logic},
booktitle={Types for Proofs and Programs (TYPES 2000)},
editor={P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
year=2002,publisher=Springer,series=LNCS,volume=2277,pages="24--40"}

@inproceedings{HaftmannN-FLOPS2010,
author={Florian Haftmann and Tobias Nipkow},
title={Code Generation via Higher-Order Rewrite Systems},
booktitle={Functional and Logic Programming (FLOPS 2010)},
editor={M. Blume and N. Kobayashi and G. Vidal},
publisher=Springer,series=LNCS,volume={6009},pages={103-117},year=2010}

@inproceedings{HaftmannKKN-ITP13,
author={Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
title={Data Refinement in \mbox{Isabelle/HOL}},
booktitle={ITP 2013},editor={S. Blazy and C. Paulin-Mohring and D. Pichardie},
publisher=Springer,series=LNCS,volume={7998},pages={100-115},year=2013}

@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman},
title={Introduction to Automata Theory, Languages, and Computation.},
publisher={Addison-Wesley},year=1979}

@article{Knuth71,
  author    = {Donald E. Knuth},
  title     = {Optimum Binary Search Trees},
  journal   = {Acta Inf.},
  volume    = {1},
  pages     = {14--25},
  year      = {1971}}

@book{Concrete,author={Tobias Nipkow and Gerwin Klein},
title="Concrete Semantics with Isabelle/HOL",publisher="Springer",year=2014,
note={\url{http://concrete-semantics.org}}}

@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher="Springer",series="LNCS",volume=2283,year=2002}

@article{monadification,
title = "Monadification of functional programs",
journal = "Science of Computer Programming",
volume = "52",
number = "1",
pages = "101 - 129",
year = "2004",
note = "Special Issue on Program Transformation",
issn = "0167-6423",
doi = "https://doi.org/10.1016/j.scico.2004.03.004",
url = "http://www.sciencedirect.com/science/article/pii/S0167642304000486",
author = "Martin Erwig and Deling Ren"
}

@inproceedings{Itzhaky16,
 author = {Itzhaky, Shachar and Singh, Rohit and Solar-Lezama, Armando and Yessenov, Kuat and Lu, Yongquan and Leiserson, Charles and Chowdhury, Rezaul},
 title = {Deriving Divide-and-conquer Dynamic Programming Algorithms Using Solver-aided Transformations},
 booktitle = {Proc.\ 2016 ACM SIGPLAN Int.\ Conf.\ Object-Oriented Programming, Systems, Languages, and Applications},
 series = {OOPSLA 2016},
 year = {2016},
 location = {Amsterdam, Netherlands},
 pages = {145--164},
 numpages = {20},
 url = {http://doi.acm.org/10.1145/2983990.2983993},
 doi = {10.1145/2983990.2983993},
 acmid = {2983993},
 publisher = {ACM}
}

@inproceedings{Wadler89,
 author = {Wadler, Philip},
 title = {Theorems for Free!},
 booktitle = {Proc.\ Fourth Int.\ Conf.\ Functional Programming Languages and Computer Architecture},
 series = {FPCA '89},
 year = {1989},
 isbn = {0-89791-328-0},
 location = {Imperial College, London, United Kingdom},
 pages = {347--359},
 numpages = {13},
 url = {http://doi.acm.org.eaccess.ub.tum.de/10.1145/99370.99404},
 doi = {10.1145/99370.99404},
 acmid = {99404},
 publisher = {ACM}
}

@inproceedings{Reynolds83,
  author    = {John C. Reynolds},
  title     = {Types, Abstraction and Parametric Polymorphism},
  booktitle = {{IFIP} Congress},
  pages     = {513--523},
  year      = {1983},
  timestamp = {Thu, 03 Jan 2002 12:03:25 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/ifip/Reynolds83},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@phdthesis{Krauss2009,
  author    = {Alexander Krauss},
  title     = {Automating Recursive Definitions and Termination Proofs in Higher-Order
               Logic},
  school    = {Technical University Munich},
  year      = {2009},
  url       = {http://mediatum2.ub.tum.de/doc/681651/document.pdf},
  urn       = {urn:nbn:de:bvb:91-diss-20090722-681651-1-1},
  timestamp = {Fri, 02 Dec 2016 13:44:30 +0100},
  biburl    = {http://dblp.org/rec/bib/phd/de/Krauss2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@phdthesis{Slind99,
  author    = {Konrad Slind},
  title     = {Reasoning about terminating functional programs},
  school    = {Technical University Munich, Germany},
  year      = {1999},
  url       = {https://mediatum.ub.tum.de/node?id=601660},
  urn       = {urn:nbn:de:bvb:91-diss1999111516455},
  timestamp = {Tue, 17 Jan 2017 13:51:53 +0100},
  biburl    = {http://dblp.org/rec/bib/phd/dnb/Slind99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{imperative-hol,
  author    = {Lukas Bulwahn and
               Alexander Krauss and
               Florian Haftmann and
               Levent Erk{\"{o}}k and
               John Matthews},
  title     = {Imperative Functional Programming with {Isabelle/HOL}},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2008)},
  pages     = {134--149},
  year      = {2008},
  doi       = {10.1007/978-3-540-71067-7_14},
}

@book{Kleinberg-Tardos,
  author    = {Jon M. Kleinberg and
               {\'{E}}va Tardos},
  title     = {Algorithm Design},
  publisher = {Addison-Wesley},
  year      = {2006},
  isbn      = {978-0-321-37291-8},
  timestamp = {Wed, 23 Mar 2011 16:58:37 +0100},
  biburl    = {http://dblp.org/rec/bib/books/daglib/0015106},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@phdthesis{Kuncar16,
  author    = {Ondrej Kuncar},
  title     = {Types, Abstraction and Parametric Polymorphism in Higher-Order Logic},
  school    = {Technical University Munich, Germany},
  year      = {2016},
  url       = {http://nbn-resolving.de/urn:nbn:de:bvb:91-diss-20160408-1285267-1-5},
  urn       = {urn:nbn:de:bvb:91-diss-20160408-1285267-1-5},
  timestamp = {Wed, 09 Nov 2016 14:06:32 +0100},
  biburl    = {http://dblp.org/rec/bib/phd/dnb/Kuncar16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{HatcliffD94,
  author    = {John Hatcliff and
               Olivier Danvy},
  title     = {A Generic Account of Continuation-Passing Styles},
  booktitle = {Conf.\ Record of POPL'94: 21st {ACM} {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages},
  pages     = {458--471},
  year      = {1994},
  url       = {http://doi.acm.org/10.1145/174675.178053},
  doi       = {10.1145/174675.178053},
  timestamp = {Mon, 21 May 2012 16:19:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/HatcliffD94},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{VermaGPA00,
  author    = {Kumar Neeraj Verma and
               Jean Goubault{-}Larrecq and
               Sanjiva Prasad and
               S. Arun{-}Kumar},
  title     = {Reflecting {BDDs} in {Coq}},
  booktitle = {Advances in Computing Science - {ASIAN} 2000},
  pages     = {162--181},
  year      = {2000},
  editor    = {Jifeng He and
               Masahiko Sato},
  series    = LNCS,
  volume    = {1961},
  publisher = {Springer},
}

@article{BraibantJM14,
  author    = {Thomas Braibant and
               Jacques{-}Henri Jourdan and
               David Monniaux},
  title     = {Implementing and Reasoning About Hash-consed Data Structures in {Coq}},
  journal   = {J. Autom. Reasoning},
  volume    = {53},
  number    = {3},
  pages     = {271--304},
  year      = {2014},
  url       = {https://doi.org/10.1007/s10817-014-9306-0},
  doi       = {10.1007/s10817-014-9306-0},
  timestamp = {Sat, 20 May 2017 00:22:32 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/BraibantJM14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Michie68, author={Michie, Donald}, title={Memo Functions and Machine Learning}, journal={Nature},
volume=218,pages={19--22},year=1968}

@inproceedings{IRF,
author = {Lammich, Peter},
booktitle = {{ITP} 2015, Proceedings},
doi = {10.1007/978-3-319-22102-1_17},
editor = {Urban, Christian and Zhang, Xingyuan},
isbn = {978-3-319-22101-4},
pages = {253--269},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Refinement to {Imperative/HOL}},
volume = {9236},
year = {2015}
}

@article{CYK-AFP,
  author  = {Maksym Bortin},
  title   = {A formalisation of the Cocke-Younger-Kasami algorithm},
  journal = {Archive of Formal Proofs},
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/CYK.html},
            Formal proof development},
}

@inproceedings{DP-ITP-2018,
author  = {Wimmer, Simon and Hu, Shuwei and Nipkow, Tobias},
booktitle = {{ITP} 2018, Proceedings},
editor = {Avigad, Jeremy and Mahboubi, Assia},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title   = {Verified Memoization and Dynamic Programming},
year = {2018}
}