[Colloquium] Arthur Vale - MS Presentation on August 8th

[Karin Czaplewski]

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

Abstract: 

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


Karin Czaplewski
Student & Faculty Services Specialist
Masters Program in Computer Science
The University of Chicago
Crerar Library 328
5730 S. Ellis Avenue
Office: 773.834.8587
https://masters.cs.uchicago.edu <https://masters.cs.uchicago.edu/>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20190806/de624dc0/attachment-0001.html>