@incollection(sep-brouwer,
 author       = {Mark van Atten},
 year         = {2020},
 title        = {{Luitzen Egbertus Jan Brouwer}},
 editor       = {Edward N. Zalta},
 booktitle    = {The {Stanford} Encyclopedia of Philosophy},
 edition      = {{S}pring 2020},
 publisher    = {Metaphysics Research Lab, Stanford University},
)
@article(BasinMV98,
 author       = {David A. Basin and Se{\'{a}}n Matthews and Luca Vigan{\`{o}}},
 year         = {1998},
 title        = {Labelled Modal Logics: Quantifiers},
 journal      = {Journal of Logic, Language and Information},
 volume       = {7},
 number       = {3},
 pages        = {237--263},
 doi          = {10.1023/A:1008278803780},
)
@inproceedings(Isar08,
 author       = {Stefan Berghofer and Makarius Wenzel},
 year         = {2008},
 title        = {Logic-Free Reasoning in {Isabelle/Isar}},
 editor       = {Serge Autexier and John A. Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk},
 booktitle    = {Intelligent Computer Mathematics, 9th International Conference, {AISC} 2008, 15th Symposium, Calculemus 2008, 7th International Conference, {MKM} 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5144},
 publisher    = {Springer},
 pages        = {355--369},
 doi          = {10.1007/978-3-540-85110-3\_31},
)
@article(DionisioGM05,
 author       = {F. Miguel Dion\'{i}sio and Paula Gouveia and Jo{\~{a}}o Marcos},
 year         = {2005},
 title        = {Defining and using deductive systems with {Isabelle}},
 journal      = {Computing, Philosophy, and Cognition},
 pages        = {271--293},
)
@incollection(dummett1975philosophical,
 author       = {Michael Dummett},
 year         = {1975},
 title        = {The philosophical basis of intuitionistic logic},
 booktitle    = {Studies in Logic and the Foundations of Mathematics},
 volume       = {80},
 publisher    = {Elsevier},
 pages        = {5--40},
)
@book(dummett2000elements,
 author       = {Michael Dummett},
 year         = {2000},
 title        = {Elements of intuitionism},
 publisher    = {Oxford University Press},
)
@inproceedings(ThEdu19,
 author       = {Asta Halkj{\ae}r From and Alexander Birch Jensen and Anders Schlichtkrull and J{\o}rgen Villadsen},
 year         = {2019},
 title        = {Teaching a Formalized Logical Calculus},
 editor       = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
 booktitle    = {Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019},
 series       = {{EPTCS}},
 volume       = {313},
 pages        = {73--92},
 doi          = {10.4204/EPTCS.313.5},
)
@inproceedings(ThEdu20,
 author       = {Asta Halkj{\ae}r From and J{\o}rgen Villadsen and Patrick Blackburn},
 year         = {2020},
 title        = {Isabelle/{HOL} as a Meta-Language for Teaching Logic},
 editor       = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
 booktitle    = {Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020},
 series       = {{EPTCS}},
 volume       = {328},
 pages        = {18--34},
 doi          = {10.4204/EPTCS.328.2},
)
@article(FOL-Axiomatic-AFP,
 author       = {Asta Halkj\IeC{\ae}r From},
 year         = {2021},
 title        = {Soundness and Completeness of an Axiomatic System for First-Order Logic},
 journal      = {Archive of Formal Proofs},
 note         = {\url{https://isa-afp.org/entries/FOL_Axiomatic.html}, Formal proof development},
)
@incollection(sep-intuitionism,
 author       = {Rosalie Iemhoff},
 year         = {2020},
 title        = {{Intuitionism in the Philosophy of Mathematics}},
 editor       = {Edward N. Zalta},
 booktitle    = {The {Stanford} Encyclopedia of Philosophy},
 edition      = {{F}all 2020},
 publisher    = {Metaphysics Research Lab, Stanford University},
)
@incollection(sep-logic-intuitionistic,
 author       = {Joan Moschovakis},
 year         = {2021},
 title        = {{Intuitionistic Logic}},
 editor       = {Edward N. Zalta},
 booktitle    = {The {Stanford} Encyclopedia of Philosophy},
 edition      = {{F}all 2021},
 publisher    = {Metaphysics Research Lab, Stanford University},
)
@book(nipkow+02,
 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},
)
@article(Paulson89,
 author       = {Lawrence C. Paulson},
 year         = {1989},
 title        = {The Foundation of a Generic Theorem Prover},
 journal      = {J. Autom. Reason.},
 volume       = {5},
 number       = {3},
 pages        = {363--397},
 doi          = {10.1007/BF00248324},
)
@inproceedings(ThEdu18,
 author       = {Anders Schlichtkrull and J{\o}rgen Villadsen and Andreas Halkj{\ae}r From},
 year         = {2018},
 title        = {Students' Proof Assistant {(SPA)}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 7th International Workshop on Theorem proving components for Educational software, THedu@FLoC 2018, Oxford, United Kingdom, 18 july 2018},
 series       = {{EPTCS}},
 volume       = {290},
 pages        = {1--13},
 doi          = {10.4204/EPTCS.290.1},
)
@inproceedings(ThEdu17,
 author       = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2017},
 title        = {Natural Deduction and the {Isabelle} Proof Assistant},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017},
 series       = {{EPTCS}},
 volume       = {267},
 pages        = {140--155},
 doi          = {10.4204/EPTCS.267.9},
)
@inproceedings(PAAR,
 author       = {J{\o}rgen Villadsen and Anders Schlichtkrull and Andreas Halkj{\ae}r From},
 year         = {2018},
 title        = {A Verified Simple Prover for First-Order Logic},
 editor       = {Boris Konev and Josef Urban and Philipp R{\"{u}}mmer},
 booktitle    = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR 2018) co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, 19 July 2018},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {2162},
 publisher    = {CEUR-WS.org},
 pages        = {88--104},
 url          = {http://ceur-ws.org/Vol-2162/paper-08.pdf},
)
@inproceedings(Pure08,
 author       = {Makarius Wenzel and Lawrence C. Paulson and Tobias Nipkow},
 year         = {2008},
 title        = {The {Isabelle} Framework},
 editor       = {Otmane A{\"{\i}}t Mohamed and Mu{\~{n}}oz, C{\'{e}}sar A. and Sofi{\`{e}}ne Tahar},
 booktitle    = {Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {33--38},
 doi          = {10.1007/978-3-540-71067-7\_7},
)