Proust: A Nano Proof Assistant

Prabhakar Ragde
(University of Waterloo)

Proust is a small Racket program offering rudimentary interactive assistance in the development of verified proofs for propositional and predicate logic. It is constructed in stages, some of which are done by students before using it to complete proof exercises, and in parallel with the study of its theoretical underpinnings, including elements of Martin-Lof type theory. The goal is twofold: to demystify some of the machinery behind full-featured proof assistants such as Coq and Agda, and to better integrate the study of formal logic with other core elements of an undergraduate computer science curriculum.

In Johan Jeuring and Jay McCarthy: Proceedings of the 4th and 5th International Workshop on Trends in Functional Programming in Education (TFPIE 2015/6), Sophia-Antipolis, France and University of Maryland College Park, USA, 2nd June 2015 and 7th June 2016, Electronic Proceedings in Theoretical Computer Science 230, pp. 63–75.
Published: 26th November 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.230.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org