λ' is Confluent
Master thesis
![Thumbnail](/bora-xmlui/bitstream/handle/11250/3116034/3250096.pdf.jpg?sequence=3&isAllowed=y)
View/ Open
Date
2023-11-20Metadata
Show full item recordCollections
- Master theses [202]
Abstract
The λ-calculus is a well-known model of computation, characterised by its simplicity and adapted for the implementation of functional programming languages. We present an extension of the λ-calculus proposed by Gylterud, λ'-calculus, with primitive quotation operations to allow for internalised self-interpretation, a form of metaprogramming. Using the proof assistant Agda, we give a formalisation of its syntax and operational semantics and prove confluence, a property which gives any reducible term a unique normal form.