Our work strives to demonstrate that a language type checker can be an effective tool in teaching language design. We have used TypeSoundnessCertifier, a tool for type checking language definitions and certifying their soundness, in the context of an instance of a course in programming languages. In this short paper, we offer details on how the course took place, and report on some data gathered during some evaluations. Although the work reported in this paper is not statistically significant, we hope to inspire our colleagues to adopt a language type checker such as TypeSoundnessCertifier in their courses in programming languages.

Matteo Cimini is an assistant professor at the Department of Computer Science at University of Massachusetts Lowell. His research interests span programming languages and formal methods, with a particular focus in gradual typing, and the analysis of programs and languages.