<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">This is an announcement of Arthur Vale's MS Presentation. Arthur is a student in the Bx/MS program.<div class=""><br class=""></div><div class="">===========================================================================</div><div class="">Date:<span class="Apple-tab-span" style="white-space:pre"> </span>Thursday, August 8, 2019 </div><div class=""><br class=""></div><div class="">Time:<span class="Apple-tab-span" style="white-space:pre"> </span>TBA<br class=""><br class=""></div><div class="">Place:<span class="Apple-tab-span" style="white-space:pre"> </span>John Crerar Library 298</div><div class=""><br class=""></div><div class="">M.S. Candidate:<span class="Apple-tab-span" style="white-space:pre"> </span>Arthur Vale</div><div class=""><br class="">M.S. Paper Title: Abstracting Syntax for Meta-Theoretic Proof-Carrying Programming Languages Implementation<br class=""><br class="">Abstract: </div><div class=""><br class="">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.<br class=""><br class="">Arthur’s Adviser: Professor Stuart Kurtz<br class=""><div class=""><br class=""></div><div class=""><br class=""><div class="">
<div dir="auto" style="text-align: start; text-indent: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="auto" style="text-align: start; text-indent: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="text-align: start; text-indent: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="text-align: start; text-indent: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="text-align: start; text-indent: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="text-align: start; text-indent: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div style="font-variant-ligatures: normal; font-variant-position: normal; font-variant-numeric: normal; font-variant-alternates: normal; font-variant-east-asian: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; widows: 2; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; font-weight: normal; margin: 0in 0in 0.0001pt;"><b class=""><span class="" style="font-family: "Mongolian Baiti"; color: rgb(139, 0, 33); font-size: 13px;">Karin Czaplewski</span></b></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; margin: 0in 0in 0.0001pt;"><span class="" style="text-align: -webkit-auto;"><span class="" style="font-family: "Mongolian Baiti"; color: rgb(119, 117, 116); font-size: 13px;">Student & Faculty Services Specialist</span></span></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; margin: 0in 0in 0.0001pt;"><b class=""><span class="" style="font-family: "Mongolian Baiti"; color: rgb(119, 117, 116); font-size: 13px;">Masters Program in Computer Science</span></b></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; font-weight: normal; margin: 0in 0in 0.0001pt;"><b class=""><span class="" style="font-family: "Mongolian Baiti"; color: rgb(119, 117, 116); font-size: 13px;">The University of Chicago</span></b></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; font-weight: normal; margin: 0in 0in 0.0001pt;"><span class="" style="color: rgb(119, 117, 116); font-family: "Mongolian Baiti"; font-size: 13px;">Crerar Library 328</span></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; font-weight: normal; margin: 0in 0in 0.0001pt;"><span class="" style="color: rgb(119, 117, 116); font-family: "Mongolian Baiti"; font-size: 13px;">5730 S. Ellis Avenue</span></div><div class="" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-style: normal; font-variant-caps: normal; letter-spacing: normal; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none; -webkit-text-stroke-width: 0px; font-weight: normal; margin: 0in 0in 0.0001pt;"><span class="" style="color: rgb(119, 117, 116); font-family: "Mongolian Baiti"; font-size: 13px;">Office: 773.834.8587</span></div><div class="" style="margin: 0in 0in 0.0001pt;"><a href="https://masters.cs.uchicago.edu/" class="">https://masters.cs.uchicago.edu</a></div><div class="" style="margin: 0in 0in 0.0001pt;"><br class=""></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></body></html>