@article{blanchette2016lambda,
  author  = {Jasmin Christian Blanchette and Uwe Waldmann and Daniel Wand},
  title   = {Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Lambda_Free_RPOs.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@InProceedings{hupel2018compiler,
author="Hupel, Lars
and Nipkow, Tobias",
editor="Ahmed, Amal",
title="A Verified Compiler from Isabelle/HOL to CakeML",
booktitle="Programming Languages and Systems",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="999--1026",
abstract="Many theorem provers can generate functional programs from definitions or proofs. However, this code generation needs to be trusted. Except for the HOL4 system, which has a proof producing code generator for a subset of ML. We go one step further and provide a verified compiler from Isabelle/HOL to CakeML. More precisely we combine a simple proof producing translation of recursion equations in Isabelle/HOL into a deeply embedded term language with a fully verified compilation chain to the target language CakeML.",
isbn="978-3-319-89884-1"
}

@article{sternagel2015deriving,
  author  = {Christian Sternagel and René Thiemann},
  title   = {Deriving class instances for datatypes},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Deriving.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@Article{urban2013nominal,
  author  = {Christian Urban and Stefan Berghofer and Cezary Kaliszyk},
  title   = {Nominal 2},
  journal = {Archive of Formal Proofs},
  year    = {2013},
  month   = feb,
  note    = {\url{http://isa-afp.org/entries/Nominal2.shtml}, Formal proof development},
  issn    = {2150-914x},
}

@Article{urban2008nominal,
  author   = {Urban, Christian},
  title    = {Nominal Techniques in {Isabelle/HOL}},
  journal  = {Journal of Automated Reasoning},
  year     = {2008},
  volume   = {40},
  number   = {4},
  pages    = {327--356},
  abstract = {This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover using nominal techniques. Central to the formalisation is an inductive set that is bijective with the alpha-equated lambda-terms. Unlike de-Bruijn indices, however, this inductive set includes names and reasoning about it is very similar to informal reasoning with ``pencil and paper''. To show this we provide a structural induction principle that requires to prove the lambda-case for fresh binders only. Furthermore, we adapt work by Pitts providing a recursion combinator for the inductive set. The main technical novelty of this work is that it is compatible with the axiom of choice (unlike earlier nominal logic work by Pitts et al); thus we were able to implement all results in Isabelle/HOL and use them to formalise the standard proofs for Church-Rosser, strong-normalisation of beta-reduction, the correctness of the type-inference algorithm W, typical proofs from SOS and much more.},
  doi      = {10.1007/s10817-008-9097-2},
  issn     = {1573-0670},
  url      = {http://dx.doi.org/10.1007/s10817-008-9097-2},
}

@TechReport{schmidt1988unification,
  author      = {Manfred Schmidt-Schau{\ss} and J\"org Siekmann},
  title       = {Unification Algebras: An Axiomatic Approach to Unification, Equation Solving and Constraint Solving},
  institution = {FB Informatik, Universit\"at Kaiserslautern},
  year        = {1988},
  number      = {SEKI-report SR-88-09},
  url         = {http://www.ki.informatik.uni-frankfurt.de/papers/schauss/unif-algebr.pdf},
}

@Article{eder1985properties,
  author    = {Elmar Eder},
  title     = {Properties of substitutions and unifications},
  journal   = {Journal of Symbolic Computation},
  year      = {1985},
  volume    = {1},
  number    = {1},
  pages     = {31--46},
  month     = {mar},
  doi       = {10.1016/s0747-7171(85)80027-4},
  publisher = {Elsevier {BV}},
}

@article{sternagel2018terms,
  author  = {Christian Sternagel and René Thiemann},
  title   = {First-Order Terms},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/First_Order_Terms.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@Book{williams1991instantiation,
  title     = {Instantiation Theory},
  publisher = {Springer-Verlag},
  year      = {1991},
  author    = {James G. Williams},
  doi       = {10.1007/bfb0031932},
  url       = {https://doi.org/10.1007%2Fbfb0031932},
}