@unpublished(dedukti,
 author       = {Ali Assaf and Guillaume Burel and Rapha\"el Cauderlier and Gilles Dowek and Catherine Dubois and Fr\'ed\'eric Gilbert and Pierre Halmagrand and Olivier Hermant and Ronan Saillard},
 title        = {Dedukti: a {Logical} {Framework} based on the $\lambda\Pi $-{Calculus} {Modulo} {Theory}},
 url          = {http://www.lsv.fr/~dowek/Publi/expressing.pdf},
)
@inproceedings(zenon,
 author       = {Richard Bonichon and David Delahaye and Damien Doligez},
 year         = {2007},
 title        = {Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, {LPAR} 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings},
 pages        = {151--165},
 doi          = {10.1007/978-3-540-75560-9\_13},
)
@unpublished(buryarchsat,
 author       = {Guillaume Bury and Simon Cruanes and David Delahaye},
 year         = {2018},
 title        = {{SMT Solving Modulo Tableau and Rewriting Theories}},
 url          = {https://hal.archives-ouvertes.fr/hal-02083232},
)
@phdthesis(zipperposition,
 author       = {Simon Cruanes},
 year         = {2015},
 title        = {{Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond}},
 type         = {Theses},
 school       = {{{\'E}cole polytechnique}},
 url          = {https://hal.archives-ouvertes.fr/tel-01223502},
)
@inproceedings(zenonmodulo,
 author       = {David Delahaye and Damien Doligez and Fr\'ed\'eric Gilbert and Pierre Halmagrand and Olivier Hermant},
 year         = {2013},
 title        = {Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo},
 editor       = {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {274--290},
 doi          = {10.1007/978-3-642-45221-5_20},
)
@unpublished(dowek,
 author       = {Gilles Dowek and Benjamin Werner},
 title        = {A constructive proof of {Skolem} theorem for constructive logic},
 url          = {http://www.lsv.fr/~dowek/Publi/skolem.pdf},
)
@inproceedings(Schulz:LPAR-2013,
 author       = {Stephan Schulz},
 year         = {2013},
 title        = {{System Description: E~1.8}},
 editor       = {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
 booktitle    = {Proc.\ of the 19th LPAR, Stellenbosch},
 series       = {LNCS},
 volume       = {8312},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-45221-5_49},
)
@article(Sut17,
 author       = {G. Sutcliffe},
 year         = {2017},
 title        = {{The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0}},
 journal      = {Journal of Automated Reasoning},
 volume       = {59},
 number       = {4},
 pages        = {483--502},
 doi          = {10.1007/s10817-017-9407-7},
)
@article(casc,
 author       = {Geoff Sutcliffe},
 year         = {2018},
 title        = {The 9th {IJCAR} Automated Theorem Proving System Competition - {CASC-J9}},
 journal      = {{AI} Commun.},
 volume       = {31},
 number       = {6},
 pages        = {495--507},
 doi          = {10.3233/AIC-180773},
)
@inproceedings(thire18sharing,
 author       = {Fran{\c{c}}ois Thir{\'{e}}},
 year         = {2018},
 title        = {Sharing a Library between Proof Assistants: Reaching out to the {HOL} Family},
 editor       = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis},
 booktitle    = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018.},
 series       = {{EPTCS}},
 volume       = {274},
 pages        = {57--71},
 doi          = {10.4204/EPTCS.274.5},
)