@inproceedings{bla-compl,
title = "Unified Classical Logic Completeness: A Coinductive Pearl",
author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
year = 2014,
publisher = "Springer",
editor = "St{\'e}phane Demri and Deepak Kapur and Christoph Weidenbach",
booktitle = "IJCAR 2014",
series = "LNCS"
}

@inproceedings{bla-mech,
  author    = {Jasmin Christian Blanchette and Andrei Popescu},
  title     = {Mechanizing the Metatheory of Sledgehammer},
  booktitle = {FroCoS 2013},
  year      = {2013},
  pages     = {245--260},
  editor    = {Pascal Fontaine and
               Christophe Ringeissen and
               Renate A. Schmidt},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {8152}
}