@misc(proofweb,
 title        = {ProofWeb. (ProofWeb is both a system for teaching logic and for using proof assistants through the web).},
 url          = {http://proofweb.cs.ru.nl/login.php},
 note         = {Accessed December 2017},
)
@article(Berghofer,
 author       = {Stefan Berghofer},
 year         = {2007},
 title        = {First-Order Logic According to Fitting},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/FOL-Fitting.html}, Formal proof development},
)
@inproceedings(Blanchette,
 author       = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
 year         = {2014},
 title        = {Unified Classical Logic Completeness - {A} Coinductive Pearl},
 series       = {Lecture Notes in Computer Science},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {46--60},
 doi          = {10.1007/978-3-319-08587-6_4},
)
@inproceedings(breitner,
 author       = {Joachim Breitner},
 year         = {2016},
 title        = {Visual Theorem Proving with the Incredible Proof Machine},
 booktitle    = {Interactive Theorem Proving - 7th International Conference, {ITP} 2016, Nancy, France, August 22-25, 2016, Proceedings},
 pages        = {123--139},
 doi          = {10.1007/978-3-319-43144-4_8},
)
@article(IncredibleProofMachineAFP,
 author       = {Joachim Breitner and Denis Lohner},
 year         = {2016},
 title        = {The meta theory of the Incredible Proof Machine},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Incredible_Proof_Machine.html}, Formal proof development},
)
@article(pandora,
 author       = {Krysia Broda and Jiefei Ma and Gabrielle Sinnadurai and Alexander J. Summers},
 year         = {2007},
 title        = {Pandora: {A} Reasoning Toolbox using Natural Deduction Style},
 journal      = {Logic Journal of the {IGPL}},
 volume       = {15},
 number       = {4},
 pages        = {293--304},
 doi          = {10.1093/jigpal/jzm020},
)
@inproceedings(Elsman,
 author       = {Martin Elsman},
 year         = {2011},
 title        = {SMLtoJs: Hosting a Standard ML Compiler in a Web Browser},
 booktitle    = {Proceedings of the 1st ACM SIGPLAN International Workshop on Programming Language and Systems Technologies for Internet Clients},
 series       = {PLASTIC '11},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {39--48},
 doi          = {10.1145/2093328.2093336},
)
@book(Fitting,
 author       = {Melvin Fitting},
 year         = {1996},
 title        = {First-Order Logic and Automated Theorem Proving, Second Edition},
 series       = {Graduate Texts in Computer Science},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4612-2360-3},
)
@(From,
 author       = {Andreas Halkj{\ae}r From},
 year         = {2017},
 title        = {Formalized First-Order Logic},
 note         = {BSc Thesis, Technical University of Denmark},
)
@inproceedings(panda,
 author       = {Olivier Gasquet and Fran{\c{c}}ois Schwarzentruber and Martin Strecker},
 year         = {2011},
 title        = {Panda: {A} Proof Assistant in Natural Deduction for All. {A} Gentzen Style Proof Assistant for Undergraduate Students},
 series       = {Lecture Notes in Computer Science},
 volume       = {6680},
 publisher    = {Springer},
 pages        = {85--92},
 doi          = {10.1007/978-3-642-21350-2_11},
)
@inproceedings(Harrison,
 author       = {John Harrison},
 year         = {1998},
 title        = {Formalizing Basic First Order Model Theory},
 booktitle    = {Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings},
 publisher    = {Springer},
 pages        = {153--170},
 doi          = {10.1007/BFb0055135},
)
@book(Huth,
 author       = {Michael Huth and Mark Ryan},
 year         = {2004},
 title        = {Logic in Computer Science: Modelling and Reasoning about Systems. Second Edition},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511810275},
)
@article(FOLHarrisonAFP,
 author       = {Alexander Birch Jensen and Anders Schlichtkrull and J{\o}rgen Villadsen},
 year         = {2017},
 title        = {First-Order Logic According to Harrison},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/FOL_Harrison.html}, Formal proof development},
)
@inproceedings(Kumar,
 author       = {Ramana Kumar and Rob Arthan and Magnus O. Myreen and Scott Owens},
 year         = {2014},
 title        = {{HOL} with Definitions: Semantics, Soundness, and a Verified Implementation},
 series       = {Lecture Notes in Computer Science},
 volume       = {8858},
 publisher    = {Springer},
 pages        = {308--324},
 doi          = {10.1007/978-3-319-08970-6_20},
)
@book(Klein,
 author       = {Tobias Nipkow and Gerwin Klein},
 year         = {2014},
 title        = {Concrete Semantics - With Isabelle/HOL},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-10542-0},
)
@book(Nipkow,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(kjs,
 author       = {Daejun Park and Stef\u{a}nescu, Andrei and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {KJS: A Complete Formal Semantics of JavaScript},
 booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series       = {PLDI '15},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {346--356},
 doi          = {10.1145/2737924.2737991},
)
@article(Seldin,
 author       = {Jonathan P. Seldin},
 year         = {1989},
 title        = {Normalization and excluded middle. {I}},
 journal      = {Studia Logica},
 volume       = {48},
 number       = {2},
 pages        = {193--217},
 doi          = {10.1007/BF02770512},
)
@article(IFCoLog,
 author       = {J{\o}rgen Villadsen and Alexander Birch Jensen and Anders Schlichtkrull},
 year         = {2017},
 title        = {{NaDeA}: {A} Natural Deduction Assistant with a Formalization in Isabelle},
 journal      = {IFCoLog Journal of Logics and their Applications},
 volume       = {4},
 number       = {1},
 pages        = {55--82},
)
@misc(Isar,
 author       = {Makarius Wenzel},
 year         = {2017},
 title        = {The {Isabelle/Isar} Reference Manual},
 note         = {\url{http://isabelle.in.tum.de/dist/doc/isar-ref.pdf}},
)