@article{Lambda_Free_RPOs,
  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   = {September},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/Lambda_Free_RPOs.html},
             Formal proof development},
  ISSN    = {2150-914x},
}

@inproceedings{TourretFOB20,
  author       = {Sophie Tourret and
                  Pascal Fontaine and
                  Daniel El Ouraoui and
                  Haniel Barbosa},
  editor       = {Fran{\c{c}}ois Bobot and
                  Tjark Weber},
  title        = {Lifting Congruence Closure with Free Variables to {\(\lambda\)}-free
                  Higher-order Logic via {SAT} Encoding},
  booktitle    = {{SMT} 2020},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {2854},
  pages        = {3--14},
  publisher    = {CEUR-WS.org},
  year         = {2020},
  url          = {https://ceur-ws.org/Vol-2854/short1.pdf}
}

@inproceedings{BarbosaFR17,
  author       = {Haniel Barbosa and
                  Pascal Fontaine and
                  Andrew Reynolds},
  editor       = {Axel Legay and
                  Tiziana Margaria},
  title        = {Congruence Closure with Free Variables},
  booktitle    = {{TACAS} 2017},
  series       = {LNCS},
  volume       = {10206},
  pages        = {214--230},
  year         = {2017},
  doi          = {10.1007/978-3-662-54580-5\_13}
}