Thesis
Syntaxes with binding, their programs, and proofs
- Creator
- Rights statement
- Awarding institution
- University of Strathclyde
- Date of award
- 2022
- Thesis identifier
- T16605
- Person Identifier (Local)
- 201151564
- Qualification Level
- Qualification Name
- Department, School or Faculty
- Abstract
- Almost every programming language’s syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on.In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope safe operation (e.g., renaming, substitution, desugaring, printing, etc.), and then again for correctness proofs.In a case study focusing on the simply typed lambda calculus, we analyse these well scoped traversals and observe that they all share the same structure. This enables us to formulate them as instances of a more general program whose properties can be established generically. Alas, the programmer is still forced to duplicate this effort for every new language they implement.This leads us to defining an expressive universe of syntaxes with binding and to demonstrate how to implement scope safe traversals once and for all by generic programming and how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda.
- Advisor / supervisor
- McBride, Conor
- Resource Type
- DOI
Relations
Items
| Thumbnail | Title | Date Uploaded | Visibility | Actions |
|---|---|---|---|---|
|
|
PDF of thesis T16605 | 2023-06-21 | Public | Download |