Open Collections

Xu, Junfeng

University of British Columbia

When defining the syntax and semantics of programming languages, computer scientists often use some kind of computer science metanotations. These metanotations are often informal or under-defined: human readers can understand them intuitively, but they are unsuitable for use in rigorous formal proofs. The aim of this project is to develop a tool that bridges the gap between the intuitive metanotations for defining programming languages, and proof assistant languages in which properties of the languages defined can be formally proven. In this thesis, I present Redex-Plus, an implementation of a computer science metanotation based on the Racket language Redex, which is used to define programming language models. Redex-Plus is a compiler that translates language models defined in the Redex language to corresponding definitions in various proof assistant languages. Redex-Plus also generates boilerplate such as binding operations, saving the users from the tedious job of writing boilerplate by hand. Redex-Plus supports Coq, Agda, SMT-LIB, and Beluga as translation targets; it can faithfully translate language models with multiple types of bound variables; and it gives users the choice between multiple ways to represent variable binding when using the Coq or Agda targets. I evaluate Redex-Plus by formalizing a variant of Simply Typed Lambda Calculus and proving some important properties of the language model in both Coq and Agda, and by formalizing a variant of System F and attempting to prove the same properties in Coq. The source code repository of Redex-Plus is publicly available at https://gitlab.com/xujunfeng/redex-plus , and on Zenodo.

Text

2023-08-21

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/85550

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/