| dc.contributor.author | Passeniouk, Yan | |
| dc.date.accessioned | 2024-02-07T00:42:26Z | |
| dc.date.available | 2024-02-07T00:42:26Z | |
| dc.date.issued | 2023-11-20 | |
| dc.date.submitted | 2023-11-20T11:06:17Z | |
| dc.identifier | INF399 0 MAO ORD 2023 HØST | |
| dc.identifier.uri | https://hdl.handle.net/11250/3116034 | |
| dc.description.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. | |
| dc.language.iso | eng | |
| dc.publisher | The University of Bergen | |
| dc.rights | Copyright the Author. All rights reserved | |
| dc.subject | rewriting | |
| dc.subject | confluence | |
| dc.subject | agda | |
| dc.subject | type theory | |
| dc.subject | lambda | |
| dc.subject | proof assistant | |
| dc.title | λ' is Confluent | |
| dc.type | Master thesis | |
| dc.date.updated | 2023-11-20T11:06:17Z | |
| dc.rights.holder | Copyright the Author. All rights reserved | |
| dc.description.degree | Masteroppgave i informatikk | |
| dc.description.localcode | INF399 | |
| dc.description.localcode | MAMN-PROG | |
| dc.description.localcode | MAMN-INF | |
| dc.subject.nus | 754199 | |
| fs.subjectcode | INF399 | |
| fs.unitcode | 12-12-0 | |
