Thesis
A framework for semiring-annotated type systems
- Creator
- Rights statement
- Awarding institution
- University of Strathclyde
- Date of award
- 2024
- Thesis identifier
- T17017
- Person Identifier (Local)
- 201754413
- Qualification Level
- Qualification Name
- Department, School or Faculty
- Abstract
- The use of proof assistants as a tool for programming language theorists is becoming ever more practical and widespread. There is a range of satisfactory implementations of simply typed calculi in proof assistants based on dependent type theory. In this thesis, I extend an account of Simply Typed λ-calculus so as to be able to represent and reason about calculi whose variables have restricted usage patterns. Examples of such calculi include a logic with an S4 □-modality, in which certain variables cannot be used “inside” a box (□); and Linear Logic, in which linear variables have to be used exactly once. While there are existing implementations of some of these calculi in proof assistants, many of these implementations share little with the best presentations of simply typed calculi without variable usage restrictions, and thus end up being poorly understood or suboptimal in facilitating mechanised reasoning. Concretely, the main result of this thesis is a framework for representing and reasoning about a wide range of calculi with restricted variable usage. All of these calculi support novel simultaneous renaming and substitution operations. Furthermore, I provide several other examples of generic and specific programs facilitated by the framework. All of this work is implemented in the proof assistant Agda.
- Advisor / supervisor
- Atkey Bob
- Resource Type
- DOI
Relations
Items
| Thumbnail | Title | Date Uploaded | Visibility | Actions |
|---|---|---|---|---|
|
|
PDF of thesis T17017 | 2024-07-09 | Public | Download |