References

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

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org