@preamble("
  \newcommand{\doi}[1]{%\newline
    \href{http://dx.doi.org/#1}{doi:\nolinkurl{#1}}}")

@inproceedings{DBLP:conf/itp/HaftmannKKN13,
  author    = {Florian Haftmann and
               Alexander Krauss and
               Ondrej Kuncar and
               Tobias Nipkow},
  title     = {Data Refinement in {I}sabelle/{HOL}},
  booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
               2013, Rennes, France, July 22-26, 2013. Proceedings},
  year      = {2013},
  pages     = {100--115},
  crossref  = {DBLP:conf/itp/2013},
  url       = {https://doi.org/10.1007/978-3-642-39634-2_10},
  doi       = {10.1007/978-3-642-39634-2_10},
  timestamp = {Mon, 13 Oct 2014 12:39:04 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/itp/HaftmannKKN13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/itp/2013,
  editor    = {Sandrine Blazy and
               Christine Paulin{-}Mohring and
               David Pichardie},
  title     = {Interactive Theorem Proving - 4th International Conference, {ITP}
               2013, Rennes, France, July 22-26, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  year      = {2013},
  volume    = {7998},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/978-3-642-39634-2},
  doi       = {10.1007/978-3-642-39634-2},
  isbn      = {978-3-642-39633-5},
  timestamp = {Mon, 13 Oct 2014 12:39:04 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/itp/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/flops/HaftmannN10,
  author    = {Florian Haftmann and
               Tobias Nipkow},
  title     = {Code Generation via Higher-Order Rewrite Systems},
  booktitle = {Functional and Logic Programming, 10th International Symposium, {FLOPS}
               2010, Sendai, Japan, April 19-21, 2010. Proceedings},
  year      = {2010},
  pages     = {103--117},
  crossref  = {DBLP:conf/flops/2010},
  url       = {https://doi.org/10.1007/978-3-642-12251-4_9},
  doi       = {10.1007/978-3-642-12251-4_9},
  timestamp = {Mon, 13 Oct 2014 12:40:49 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/flops/HaftmannN10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/flops/2010,
  editor    = {Matthias Blume and
               Naoki Kobayashi and
               Germ{\'{a}}n Vidal},
  title     = {Functional and Logic Programming, 10th International Symposium, {FLOPS}
               2010, Sendai, Japan, April 19-21, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  year      = {2010},
  volume    = {6009},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/978-3-642-12251-4},
  doi       = {10.1007/978-3-642-12251-4},
  isbn      = {978-3-642-12250-7},
  timestamp = {Mon, 13 Oct 2014 12:40:49 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/flops/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/jar/Krauss10,
  author    = {Alexander Krauss},
  title     = {Partial and Nested Recursive Function Definitions in Higher-order
               Logic},
  journal   = {J. Autom. Reasoning},
  year      = {2010},
  volume    = {44},
  number    = {4},
  pages     = {303--336},
  url       = {https://doi.org/10.1007/s10817-009-9157-2},
  doi       = {10.1007/s10817-009-9157-2},
  timestamp = {Mon, 13 Oct 2014 12:42:59 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jar/Krauss10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/tphol/ThiemannS09,
  author    = {Ren{\'{e}} Thiemann and
               Christian Sternagel},
  title     = {Certification of Termination Proofs Using \ceta},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  year      = {2009},
  pages     = {452--468},
  crossref  = {DBLP:conf/tphol/2009},
  url       = {https://doi.org/10.1007/978-3-642-03359-9_31},
  doi       = {10.1007/978-3-642-03359-9_31},
  timestamp = {Mon, 13 Oct 2014 12:43:46 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/ThiemannS09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tphol/2009,
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  title     = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  year      = {2009},
  volume    = {5674},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/978-3-642-03359-9},
  doi       = {10.1007/978-3-642-03359-9},
  isbn      = {978-3-642-03358-2},
  timestamp = {Mon, 13 Oct 2014 12:43:46 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/cpp/HuffmanK13,
  author    = {Brian Huffman and
               Ondrej Kuncar},
  title     = {Lifting and Transfer: {A} Modular Design for Quotients in {I}sabelle/{HOL}},
  booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
               2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
  year      = {2013},
  pages     = {131--146},
  crossref  = {DBLP:conf/cpp/2013},
  url       = {https://doi.org/10.1007/978-3-319-03545-1_9},
  doi       = {10.1007/978-3-319-03545-1_9},
  timestamp = {Mon, 13 Oct 2014 12:56:37 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/HuffmanK13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cpp/2013,
  editor    = {Georges Gonthier and
               Michael Norrish},
  title     = {Certified Programs and Proofs - Third International Conference, {CPP}
               2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
  series    = {Lecture Notes in Computer Science},
  year      = {2013},
  volume    = {8307},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/978-3-319-03545-1},
  doi       = {10.1007/978-3-319-03545-1},
  isbn      = {978-3-319-03544-4},
  timestamp = {Mon, 13 Oct 2014 12:56:37 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
