Arthur Vale - MS Presentation - Abstracting Syntax for Meta-Theoretic Proof-Carrying Programming Languages Implementation

This is an announcement of Arthur Vale’s MS Presentation. Arthur is a student in the Bx/MS program.


Date: Thursday, August 8, 2019

Time: 10:30am

Place: John Crerar Library 298

M.S. Candidate: Arthur Vale

M.S. Paper Title: Abstracting Syntax for Meta-Theoretic Proof-Carrying Programming Languages Implementation


A typical programming languages research paper might involve a formal specification of a programming language, a paper proof of its meta-theory, an implementation of the programming language, and a mechanized version of the meta-theory. There is a lot of redundancy between the implementation and mechanized meta-theory. Furthermore, significant labour is necessary for the mechanization, which is most often not re-usable across different projects of the same research group. We propose an approach to programming language implementation where one implements the language to carry its own meta-theoretic proofs. This way, the same underlying implementation is both the mechanized meta-theory and the implementation. We argue that the resulting implementation can be efficient, that the mechanization can be natural and that it can be re-usable across different programming language implementations. Furthermore, we propose a couple of first-order models of abstract syntax based on locally nameless terms with cofinite quantification, and show the route to obtain basic syntactic proofs about local closure and substitution in a way that can be re-used across different programming languages. We also discuss the proof burden involved in parsing, and give a novel decidability procedure for local closure. Finally, we discuss some small examples of applications of the approach.

Arthur’s Adviser: Professor Stuart Kurtz

1 Like