@inproceedings(aldrich/simmons/shin:08sasylf,
 author       = {Jonathan Aldrich and Robert J. Simmons and Key Shin},
 year         = {2008},
 title        = {{SASyLF}: an educational proof assistant for language theory},
 booktitle    = {Workshop on Functional and Declarative Programming in Education (FDPE 2008)},
 publisher    = {ACM Press},
 address      = {New York},
 pages        = {31--40},
 doi          = {10.1145/1411260.1411266},
)
@inproceedings(ariotti/boyland:17where,
 author       = {Michael D. Ariotti and John Tang Boyland},
 year         = {2017},
 title        = {Making Substitutions Explicit in {SASyLF}},
 booktitle    = {Logical Frameworks and Meta-Languages: Theory and Practice},
 url          = {https://lfmtp.org/workshops/2017/inc/papers/paper_2_ariotti.pdf},
)
@inproceedings(aydemir/et.al:05poplmark,
 author       = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie C. Weirich and Stephan A. Zdancewic},
 year         = {2005},
 title        = {Mechanized metatheory for the masses: The {POPLmark} challenge},
 booktitle    = {Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005},
 series       = {Lecture Notes in Computer Science},
 volume       = {3603},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg, New York},
 pages        = {50--65},
 doi          = {10.1007/11541868_4},
)
@unpublished(boyland/zhao:14lf+tuples,
 author       = {John Boyland and Tian Zhao},
 year         = {2014},
 title        = {Variable-Arity Functions: Work in Progress},
 note         = {Presented at LFMTP 2014 (Vienna Summer of Logic). Available as \url{http://www.cs.uwm.edu/csfac/boyland/papers/lf+variable.pdf}},
)
@inproceedings(carter/monks:13lurch,
 author       = {Nathan Carter and Kenneth Monks},
 year         = {2013},
 title        = {Lurch: A word processor that can grade students' proofs},
 booktitle    = {Work in Progress at CICM},
 series       = {CEUR Workshop Proceedings},
 volume       = {1010},
 url          = {http://ceur-ws.org/Vol-1010/paper-04.pdf},
)
@techreport(cerna:19axolotl,
 author       = {David Cerna},
 year         = {2019},
 title        = {{AXolotl}: A Self-study Tool for First-order Logic},
 type         = {Technical Report},
 institution  = {JKU RISC},
)
@inproceedings(cerna/et.al:20mobile,
 author       = {David M. Cerna and Rafael P.D. Kiesel and Alexandra Dzhiganskaya},
 year         = {2020},
 title        = {A Mobile Application for Self-Guided Study of Formal Reasoning},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {{\rm Proceedings 8th International Workshop on} Theorem Proving Components for Educational Software, {\rm Natal, Brazil, 25th August 2019}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {313},
 publisher    = {Open Publishing Association},
 pages        = {35--53},
 doi          = {10.4204/EPTCS.313.3},
)
@article(chargueraud:11nameless,
 author       = {Arthur Chargu{\'e}raud},
 year         = {2011},
 title        = {The Locally Nameless Representation},
 journal      = {Journal of Automated Reasoning},
 pages        = {1--46},
 doi          = {10.1007/s10817-011-9225-2},
)
@article(kozen/silva:17coinduction,
 author       = {Dexter Kozen and Alexandra Silva},
 year         = {2017},
 title        = {Practical coinduction},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {27},
 number       = {7},
 pages        = {1132\IeC{\textendash}1152},
 doi          = {10.1017/S0960129515000493},
)
@article(lovas/pfenning:07refinement,
 author       = {William Lovas and Frank Pfenning},
 year         = {2008},
 title        = {A Bidirectional Refinement Type System for {LF}},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {196},
 pages        = {113\IeC{\textendash}128},
 doi          = {10.1016/j.entcs.2007.09.021},
)
@inproceedings(pfenning/elliott:88hoas,
 author       = {Frank Pfenning and Conal Elliott},
 year         = {1988},
 title        = {Higher-order abstract syntax},
 booktitle    = {Proceedings of the ACM SIGPLAN '88 Conference on Programming Language Design and Implementation},
 publisher    = {ACM Press},
 address      = {New York},
 pages        = {199--208},
 doi          = {10.1145/53990.54010},
)
@misc(pfenning/schuermann:02twelf,
 author       = {Frank Pfenning and Carsten Sch{\"u}rmann},
 year         = {2002},
 title        = {Twelf User's Guide, Version 1.4},
 howpublished = {Available at \texttt{http://www.cs.cmu.edu/{\char126}twelf}},
)
@book(pierce:02types,
 author       = {Benjamin C. Pierce},
 year         = {2002},
 title        = {Types and Programming Languages},
 publisher    = {The {MIT} Press},
 address      = {Cambridge, Massachussetts, USA and London, England},
)
@inproceedings(schlichtkrull:19SPA,
 author       = {Anders Schlichtkrull and J{\o}rgen Villadsen and Andreas Halkj{\ae}r From},
 year         = {2019},
 title        = {Students' Proof Assistant (SPA)},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 7th International Workshop on} Theorem proving components for Educational software, {\rm Oxford, United Kingdom, 18 July 2018}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {290},
 publisher    = {Open Publishing Association},
 pages        = {1--13},
 doi          = {10.4204/EPTCS.290.1},
)
@book(glr,
 editor       = {Masaru Tomita},
 year         = {1991},
 title        = {Generalized LR Parsing},
 publisher    = {Springer, US},
)
@article(zhou/oliveira/zhao:20iso-recursive,
 author       = {Yaoda Zhou and Bruno C. d. S. Oliveira and Jinxu Zhao},
 year         = {2020},
 title        = {Revisiting Iso-Recursive Subtyping},
 journal      = {Proceedings of ACM Programming Languages},
 volume       = {4},
 number       = {OOPSLA},
 doi          = {10.1145/3428291},
)