@inproceedings(arawjo2017teaching,
 author       = {Ian Arawjo and Cheng-Yao Wang and Andrew C Myers and Erik Andersen and Fran{\c{c}}ois Guimbreti{\`e}re},
 year         = {2017},
 title        = {Teaching programming with gamified semantics},
 booktitle    = {Proceedings of the 2017 CHI conference on human factors in computing systems},
 pages        = {4911--4923},
 doi          = {10.1145/3025453.3025711},
)
@inproceedings(smtcoq,
 author       = {Micha{\"e}l Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Th{\'e}ry and Benjamin Werner},
 year         = {2011},
 title        = {{A modular integration of SAT/SMT solvers to Coq through proof witnesses}},
 booktitle    = {International Conference on Certified Programs and Proofs},
 organization = {Springer},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9_12},
)
@misc(smtlib,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2016},
 title        = {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
 url          = {http://www.smt-lib.org},
)
@inproceedings(breitner2016visual,
 author       = {Joachim Breitner},
 year         = {2016},
 title        = {{Visual theorem proving with the Incredible Proof Machine}},
 booktitle    = {International Conference on Interactive Theorem Proving},
 organization = {Springer},
 pages        = {123--139},
 doi          = {10.1007/978-3-319-43144-4_8},
)
@inproceedings(callies2021click,
 author       = {Etienne Callies and Olivier Laurent},
 year         = {2021},
 title        = {{Click and coLLecT An Interactive Linear Logic Prover}},
 booktitle    = {5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)},
 url          = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271501},
)
@article(axolotl,
 author       = {David M Cerna and Rafael PD Kiesel and Alexandra Dzhiganskaya},
 year         = {2020},
 title        = {A mobile application for self-guided study of formal reasoning},
 doi          = {10.48550/arXiv.2002.12553},
)
@misc(emscripten,
 author       = {Emscripten Contributors},
 year         = {2022},
 title        = {{Building to WebAssembly}},
 url          = {https://web.archive.org/web/20221030175022/https://emscripten.org/docs/compiling/WebAssembly.html},
)
@conference(z3,
 author       = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3: An efficient SMT solver}},
 booktitle    = {{International Conference on Tools and Algorithms for the Construction and Analysis of Systems}},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@inproceedings(donato2022drag,
 author       = {Pablo Donato and Pierre-Yves Strub and Benjamin Werner},
 year         = {2022},
 title        = {A drag-and-drop proof tactic},
 booktitle    = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 pages        = {197--209},
 doi          = {10.1145/3497775.3503692},
)
@mastersthesis(ehle,
 author       = {Arno Ehle},
 year         = {2017},
 title        = {Proof Search in the Sequent Calculus for First-Order Logic with Equality},
 school       = {Universit{\"a}t Kassel},
)
@article(ehle2015sequent,
 author       = {Arno Ehle and Norbert Hundeshagen and Martin Lange},
 year         = {2015},
 title        = {The sequent calculus trainer-helping students to correctly construct proofs},
 journal      = {arXiv preprint arXiv:1507.03666},
 doi          = {10.48550/arXiv.1507.03666},
)
@article(ehle2018sequent,
 author       = {Arno Ehle and Norbert Hundeshagen and Martin Lange},
 year         = {2018},
 title        = {The sequent calculus trainer with automated reasoning-helping students to find proofs},
 journal      = {arXiv preprint arXiv:1803.01467},
 doi          = {10.48550/arXiv.1803.01467},
)
@inproceedings(gasquet2011panda,
 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}},
 booktitle    = {International Congress on Tools for Teaching Logic},
 organization = {Springer},
 pages        = {85--92},
 doi          = {10.1007/978-3-642-21350-2_11},
)
@article(hoare1969axiomatic,
 author       = {Charles Antony Richard Hoare},
 year         = {1969},
 title        = {An axiomatic basis for computer programming},
 journal      = {Communications of the ACM},
 volume       = {12},
 number       = {10},
 pages        = {576--580},
 doi          = {10.1145/363235.363259},
)
@mastersthesis(seqcalc,
 author       = {Matteo Kamm and Mike Marti},
 year         = {2019},
 title        = {The Sequent Calculus Calculator},
 type         = {Bachelor's thesis},
 school       = {Hochschule f{\"u}r Technik Rapperswil},
 url          = {https://eprints.ost.ch/id/eprint/798/1/FS 2019-BA-EP-Marti-Kamm-The Sequent Calculus Calculator.pdf},
)
@misc(kaye,
 author       = {Richard W. Kaye},
 year         = {2015},
 title        = {{Proofs as structured lists and proof trees}},
 url          = {http://web.archive.org/web/20210903173847/https://web.mat.bham.ac.uk/R.W.Kaye/logic/prooftrees.html},
)
@misc(cos516,
 author       = {Zachary Kincaid},
 year         = {2021},
 title        = {{COS 516/ECE 516: Automated Reasoning about Software, Fall 2021}},
 url          = {http://web.archive.org/web/20211217155727/https://www.cs.princeton.edu/courses/archive/fall21/cos516/},
)
@article(carnap,
 author       = {Leach-Krouse, Graham},
 year         = {2018},
 title        = {Carnap: an open framework for formal reasoning in the browser},
 journal      = {arXiv preprint arXiv:1803.03092},
 doi          = {10.48550/arXiv.1803.03092},
)
@inproceedings(lerner2015polymorphic,
 author       = {Sorin Lerner and Stephen R Foster and William G Griswold},
 year         = {2015},
 title        = {{Polymorphic blocks: Formalism-inspired UI for structured connectors}},
 booktitle    = {Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems},
 pages        = {3063--3072},
 doi          = {10.1145/2702123.2702302},
)
@inproceedings(ALF,
 author       = {Lena Magnusson and Bengt Nordstr{\"o}m},
 year         = {1993},
 title        = {The {ALF} proof editor and its proof engine},
 booktitle    = {International Workshop on Types for Proofs and Programs},
 organization = {Springer},
 pages        = {213--237},
 doi          = {10.1007/3-540-58085-9_78},
)
@misc(pegjs,
 author       = {David Majda and Futago za Ryuu},
 year         = {2022},
 title        = {{PEG.js - Parser Generator for JavaScript}},
 url          = {https://web.archive.org/web/20221007224930/https://pegjs.org/},
)
@article(epigram,
 author       = {Conor McBride and James McKinna},
 year         = {2004},
 title        = {The view from the left},
 journal      = {{Journal of Functional Programming}},
 volume       = {14},
 number       = {1},
 pages        = {69--111},
 doi          = {10.1017/S0956796803004829},
)
@book(nipkow2002isabelle,
 author       = {Tobias Nipkow and Markus Wenzel and Lawrence C Paulson},
 year         = {2002},
 title        = {{Isabelle/HOL: a proof assistant for higher-order logic}},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@phdthesis(agda,
 author       = {Ulf Norell},
 year         = {2007},
 title        = {Towards a practical programming language based on dependent type theory},
 school       = {Chalmers University of Technology},
 url          = {https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
)
@article(holbert,
 author       = {Liam {O'Connor} and Rayhana Amjad},
 year         = {2022},
 title        = {Holbert: Reading, Writing, Proving and Learning in the Browser},
 journal      = {arXiv preprint arXiv:2210.11411},
 doi          = {10.48550/arXiv.2210.11411},
)
@inproceedings(sequoia,
 author       = {Giselle Reis and Zan Naeem and Mohammed Hashim},
 year         = {2020},
 title        = {Sequoia: a playground for logicians},
 booktitle    = {International Joint Conference on Automated Reasoning},
 organization = {Springer},
 pages        = {480--488},
 doi          = {10.1007/978-3-030-51054-1_32},
)
@book(Szabo69,
 editor       = {M. E. Szabo},
 year         = {1969},
 title        = {The Collected Papers of Gerhard Gentzen},
 series       = {Studies in Logic and The Foundations of Mathematics},
 publisher    = {North-Holland Publishing Company},
 address      = {Amsterdam},
)
@conference(nadea,
 author       = {J{\o}rgen Villadsen and Asta Halkj{\ae}r From and Anders Schlichtkrull},
 year         = {2019},
 title        = {{Natural Deduction Assistant (NaDeA)}},
 booktitle    = {Theorem Proving Components for Educational Software},
 doi          = {10.48550/arXiv.1904.00618},
)
@inproceedings(voronkov,
 author       = {A. A. Voronkov},
 year         = {1990},
 title        = {A proof-search method for the first order logic},
 booktitle    = {COLOG-88},
 organization = {Springer},
 pages        = {327--338},
 doi          = {10.1007/3-540-52335-9_63},
)
@article(wang,
 author       = {Hao Wang},
 year         = {1960},
 title        = {Toward mechanical mathematics},
 journal      = {{IBM Journal of Research and Development}},
 volume       = {4},
 number       = {1},
 pages        = {2--22},
 doi          = {10.1147/rd.41.0002},
)
@misc(logitext,
 author       = {Edward Z. Yang},
 year         = {2012},
 title        = {{Logitext}},
 url          = {https://github.com/ezyang/logitext},
)
@misc(fabricjs,
 author       = {Juriy Zaytsev and Stefan Kienzle and Andrea Bogazzi},
 year         = {2022},
 title        = {{Fabric.js JavaScript Canvas Library}},
 url          = {https://web.archive.org/web/20221112201025/http://fabricjs.com/},
)