Redex-plus : a metanotation for programming languages
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Xu, Junfeng
issued: 2023-08-21T18:53:15Z
issued: 2023
related degree: Master of Science - MSc
degree grantor: University of British Columbia
description: 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.
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/85550
note: REDEX-PLUS:A Metanotation for Programming LanguagesbyJunfeng XuB.Eng., Imperial College London, 2019A THESIS SUBMITTED IN PARTIAL FULFILLMENTOF THE REQUIREMENTS FOR THE DEGREE OFMaster of ScienceinTHE FACULTY OF GRADUATE AND POSTDOCTORALSTUDIES(Computer Science)The University of British Columbia(Vancouver)August 2023© Junfeng Xu, 2023The following individuals certify that they have read, and recommend to the Fac-ulty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:REDEX-PLUS:A Metanotation for Programming Languagessubmitted by Junfeng Xu in partial fulfillment of the requirements for the degreeof Master of Science in Computer Science.Examining Committee:William Bowman, Professor, Computer Science, UBCSupervisorRonald Garcia, Professor, Computer Science, UBCSupervisory Committee MemberiiAbstractWhen defining the syntax and semantics of programming languages, computer sci-entists often use some kind of computer science metanotations. These metano-tations are often informal or under-defined: human readers can understand themintuitively, but they are unsuitable for use in rigorous formal proofs. The aim ofthis project is to develop a tool that bridges the gap between the intuitive metanota-tions for defining programming languages, and proof assistant languages in whichproperties of the languages defined can be formally proven.In this thesis, I present REDEX-PLUS, an implementation of a computer sci-ence metanotation based on the Racket language Redex, which is used to defineprogramming language models. REDEX-PLUS is a compiler that translates lan-guage models defined in the Redex language to corresponding definitions in var-ious proof assistant languages. REDEX-PLUS also generates boilerplate such asbinding operations, saving the users from the tedious job of writing boilerplate byhand. REDEX-PLUS supports Coq, Agda, SMT-LIB, and Beluga as translationtargets; it can faithfully translate language models with multiple types of boundvariables; and …
has type: Thesis/Dissertation
date issued: 2023-11
is shown at: 10.14288/1.0435516
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: Attribution-NonCommercial-NoDerivatives 4.0 International
rights URI: http://creativecommons.org/licenses/by-nc-nd/4.0/
scholar level: Graduate
contributor: Bowman, William J. (Professor of computer science)
type: Text
identifier URI: http://hdl.handle.net/2429/85550