References

  1. Jonathan Aldrich, Robert J. Simmons & Key Shin (2008): SASyLF: an educational proof assistant for language theory. In: Workshop on Functional and Declarative Programming in Education (FDPE 2008). ACM Press, New York, pp. 31–40, doi:10.1145/1411260.1411266.
  2. Michael D. Ariotti & John Tang Boyland (2017): Making Substitutions Explicit in SASyLF. In: Logical Frameworks and Meta-Languages: Theory and Practice. Available at https://lfmtp.org/workshops/2017/inc/papers/paper_2_ariotti.pdf.
  3. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie C. Weirich & Stephan A. Zdancewic (2005): Mechanized metatheory for the masses: The POPLmark challenge. In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Lecture Notes in Computer Science 3603. Springer, Berlin, Heidelberg, New York, pp. 50–65, doi:10.1007/11541868_4.
  4. John Boyland & Tian Zhao (2014): Variable-Arity Functions: Work in Progress. Presented at LFMTP 2014 (Vienna Summer of Logic). Available as http://www.cs.uwm.edu/csfac/boyland/papers/lf+variable.pdf.
  5. Nathan Carter & Kenneth Monks (2013): Lurch: A word processor that can grade students' proofs. In: Work in Progress at CICM, CEUR Workshop Proceedings 1010. Available at http://ceur-ws.org/Vol-1010/paper-04.pdf.
  6. David Cerna (2019): AXolotl: A Self-study Tool for First-order Logic. Technical Report. JKU RISC.
  7. David M. Cerna, Rafael P.D. Kiesel & Alexandra Dzhiganskaya (2020): A Mobile Application for Self-Guided Study of Formal Reasoning. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313. Open Publishing Association, pp. 35–53, doi:10.4204/EPTCS.313.3.
  8. Arthur Charguéraud (2011): The Locally Nameless Representation. Journal of Automated Reasoning, pp. 1–46, doi:10.1007/s10817-011-9225-2.
  9. Dexter Kozen & Alexandra Silva (2017): Practical coinduction. Mathematical Structures in Computer Science 27(7), pp. 11321152, doi:10.1017/S0960129515000493.
  10. William Lovas & Frank Pfenning (2008): A Bidirectional Refinement Type System for LF. Electronic Notes in Theoretical Computer Science 196, pp. 113128, doi:10.1016/j.entcs.2007.09.021.
  11. Frank Pfenning & Conal Elliott (1988): Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN '88 Conference on Programming Language Design and Implementation. ACM Press, New York, pp. 199–208, doi:10.1145/53990.54010.
  12. Frank Pfenning & Carsten Schürmann (2002): Twelf User's Guide, Version 1.4. Available at http://www.cs.cmu.edu/126twelf.
  13. Benjamin C. Pierce (2002): Types and Programming Languages. The MIT Press, Cambridge, Massachussetts, USA and London, England.
  14. Anders Schlichtkrull, Jørgen Villadsen & Andreas Halkjær From (2019): Students' Proof Assistant (SPA). In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, Electronic Proceedings in Theoretical Computer Science 290. Open Publishing Association, pp. 1–13, doi:10.4204/EPTCS.290.1.
  15. Masaru Tomita (1991): Generalized LR Parsing. Springer, US.
  16. Yaoda Zhou, Bruno C. d. S. Oliveira & Jinxu Zhao (2020): Revisiting Iso-Recursive Subtyping. Proceedings of ACM Programming Languages 4(OOPSLA), doi:10.1145/3428291.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org