S. Berghofer, First-order logic according to Fitting Archive of Formal Proofs, 2007.

Y. Bertot, Filters on CoInductive Streams, an Application to Eratosthenes??? Sieve, TLCA 2005, pp.102-115, 2005.
DOI : 10.1007/11417170_9
URL : https://hal.archives-ouvertes.fr/inria-00070658

J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding monomorphic and polymorphic types, TACAS 2013, pp.493-507, 2013.
DOI : 10.1007/978-3-642-36742-7_34

J. C. Blanchette, M. Fleury, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, IJCAR 2016, 2016.
DOI : 10.24963/ijcai.2017/667
URL : https://hal.archives-ouvertes.fr/hal-01592164

J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu et al., Truly Modular (Co)datatypes for Isabelle/HOL, ITP 2014, pp.93-110, 2014.
DOI : 10.1007/978-3-319-08970-6_7

J. C. Blanchette and A. Popescu, Mechanizing the Metatheory of Sledgehammer, FroCoS 2013, pp.245-260, 2013.
DOI : 10.1007/978-3-642-40885-4_17

J. C. Blanchette, A. Popescu, and D. Traytel, Abstract completeness Archive of Formal Proofs, 2014.
DOI : 10.1007/978-3-319-20615-8_1

J. C. Blanchette, A. Popescu, and D. Traytel, Unified classical logic completeness?A coinductive pearl, IJCAR 2014, pp.46-60, 2014.
DOI : 10.1007/978-3-319-08587-6_4

J. C. Blanchette, A. Popescu, and D. Traytel, Formal development associated with this paper, 2015.

J. C. Blanchette, A. Popescu, and D. Traytel, Foundational extensible corecursion: A proof assistant perspective, pp.192-204, 2015.
DOI : 10.1145/2784731.2784732
URL : https://hal.archives-ouvertes.fr/hal-01212589

J. Brotherston, Cyclic Proofs for First-Order Logic with Inductive Definitions, TABLEAUX 2005, pp.78-92, 2005.
DOI : 10.1007/11554554_8

J. Brotherston, Sequent calculus proof systems for inductive definitions, 2006.

J. Brotherston, R. Bornat, and C. Calcagno, Cyclic proofs of program termination in separation logic, pp.101-112, 2008.

J. Brotherston, D. Distefano, and R. L. Petersen, Automated Cyclic Entailment Proofs in Separation Logic, CADE-23, pp.131-146, 2011.
DOI : 10.1007/978-3-540-70545-1_36
URL : http://www0.cs.ucl.ac.uk/staff/J.Brotherston/CADE11/ind_thm_proving_sl.pdf

J. Brotherston, N. Gorogiannis, and R. L. Petersen, A Generic Cyclic Theorem Prover, APLAS 2012, pp.350-367, 2012.
DOI : 10.1007/978-3-642-35182-2_25
URL : http://www0.cs.ucl.ac.uk/staff/J.Brotherston/APLAS12/cyclist.pdf

J. Brotherston and A. Simpson, Complete Sequent Calculi for Induction and Infinite Descent, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.51-62, 2007.
DOI : 10.1109/LICS.2007.16

A. Ciaffaglione and P. D. Gianantonio, A certified, corecursive implementation of exact real numbers, Theoretical Computer Science, vol.351, issue.1, pp.39-51, 2006.
DOI : 10.1016/j.tcs.2005.09.061
URL : https://doi.org/10.1016/j.tcs.2005.09.061

R. Diaconescu, Institution-Independent Model Theory, Studies in Universal Logic. Birkhäuser, 2008.
DOI : 10.1007/11780274_5

M. Fitting, First-Order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, 1996.
DOI : 10.1007/978-1-4684-0357-2

N. Francez, Fairness. Texts and Monographs in Computer Science, 1986.

J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Computer Science and Technology. Harper & Row, 1986.

K. Gödel, Über die Vollständigkeit des Logikkalküls, 1929.

M. J. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993.

F. Haftmann and T. Nipkow, Code Generation via Higher-Order Rewrite Systems, FLOPS 2010, pp.103-117, 2010.
DOI : 10.1007/978-3-642-12251-4_9
URL : http://isabelle.informatik.tu-muenchen.de/~nipkow/pubs/flops2010.pdf

R. Hähnle, Tableaux and related methods, Handbook of Automated Reasoning, pp.100-178, 2001.

J. Harrison, Formalizing basic first order model theory, TPHOLs '98, pp.153-170, 1998.
DOI : 10.1007/BFb0055135
URL : http://www.cl.cam.ac.uk/~jrh13/papers/model.ps.gz

D. Ilik, Constructive completeness proofs and delimited control, 2010.
URL : https://hal.archives-ouvertes.fr/tel-00529021

B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, Bull. Eur. Assoc. Theor. Comput. Sci, vol.62, pp.222-259, 1997.

S. C. Kleene, Mathematical Logic, 1967.

S. Kripke, A completeness theorem in modal logic, The Journal of Symbolic Logic, vol.XIV, issue.01, pp.1-14, 1959.
DOI : 10.2307/2964568

J. L. Krivine, Une Preuve Formelle et Intuitionniste du Th??or??me de Compl??tude de la Logique Classique, Bulletin of Symbolic Logic, vol.II, issue.04, pp.405-421, 1996.
DOI : 10.1016/0168-0072(94)90047-7

J. Margetson and T. Ridge, Completeness theorem Archive of Formal Proofs, 2004.

R. Mayr and T. Nipkow, Higher-order rewrite systems and their confluence, Theoretical Computer Science, vol.192, issue.1, pp.3-29, 1998.
DOI : 10.1016/S0304-3975(97)00143-6
URL : https://doi.org/10.1016/s0304-3975(97)00143-6

K. Nakata, T. Uustalu, and M. Bezem, A Proof Pearl with the Fan Theorem and Bar Induction, APLAS 2011, pp.353-368, 2011.
DOI : 10.1007/978-3-540-77505-8_25

S. Negri, Kripke completeness revisited Acts of Knowledge: History, Philosophy and Logic: Essays Dedicated to Göran Sundholm, pp.247-282, 2009.

T. Nipkow and G. Klein, Concrete Semantics, 2014.
DOI : 10.1007/978-3-319-10542-0

M. Petria, An institutional version of Gödel's completeness theorem, pp.409-424, 2007.
DOI : 10.1007/978-3-540-73859-6_28

F. Pfenning, Review of " Jean H. Gallier: Logic for Computer Science, J. Symb. Log, vol.22, issue.541, pp.288-289, 1986.

T. Ridge and J. Margetson, A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic, TPHOLs 2005, pp.294-309, 2005.
DOI : 10.1007/11541868_19
URL : http://www.cl.cam.ac.uk/~tjr22/doc/prover.pdf

G. Ro¸suro¸su, Equality of streams is a ? 0 2 -complete problem, p.6

G. Ro¸suro¸su, An effective algorithm for the membership problem for extended regular expressions, FoSSaCS 2007, pp.332-345, 2007.

J. J. Rutten, Automata and coinduction (an exercise in coalgebra), CONCUR '98, pp.194-218, 1998.
DOI : 10.1007/BFb0055624
URL : http://www.cwi.nl/%7Ejanr/papers/files-of-papers/1998_CONCUR_automata_and_coinduction.pdf

J. J. Rutten, Regular Expressions Revisited: A Coinductive Approach to Streams, Automata, and Power Series, MPC 2000, pp.100-101, 2000.
DOI : 10.1007/10722010_7

J. J. Rutten, Elements of Stream Calculus, Electronic Notes in Theoretical Computer Science, vol.45, pp.358-423, 2001.
DOI : 10.1016/S1571-0661(04)80972-1
URL : https://doi.org/10.1016/s1571-0661(04)80972-1

A. Schlichtkrull, Formalization of the Resolution Calculus for First-Order Logic, ITP 2016, 2016.
DOI : 10.1007/978-3-642-02959-2_10

J. J. Schlöder and P. Koepke, The Gödel completeness theorem for uncountable languages, Formalized Mathematics, vol.20, issue.3, pp.199-203, 2012.

D. Traytel, A. Popescu, and J. C. Blanchette, Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.596-605, 2012.
DOI : 10.1109/LICS.2012.75

A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2000.
DOI : 10.1017/CBO9781139168717