A Parametric Fitch-Style Modal Lambda Calculus
| dc.contributor.author | Forsman, Axel | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering | en |
| dc.contributor.examiner | Abel, Andreas | |
| dc.contributor.supervisor | Valliappan, Nachiappan | |
| dc.date.accessioned | 2024-01-12T12:30:41Z | |
| dc.date.available | 2024-01-12T12:30:41Z | |
| dc.date.issued | 2023 | |
| dc.date.submitted | 2023 | |
| dc.description.abstract | The necessity modality, denoted by , where the focus lies, has been applied to model staged computations, compartmental purity in functional languages, and more. So called Fitch-style modal deduction, where modalities are eliminated by opening a subproof, and introduced by shutting one, has been adapted for lambda calculi. Different modal logics may be encoded via different open and shut rules. Prior work [1] has given normalization proofs for four Fitch-style formulations of lambda calculi with different modalities, which required repeating the proofs for each individual calculus. A parametric Fitch-style modal lambda calculus generalizing the variants is presented, in order to avoid the repetition and ease further extensions. | |
| dc.identifier.coursecode | DATX05 | |
| dc.identifier.uri | http://hdl.handle.net/20.500.12380/307521 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Necessity | |
| dc.subject | modality | |
| dc.subject | parametric | |
| dc.subject | Fitch | |
| dc.subject | modal | |
| dc.subject | lambda calculus | |
| dc.subject | normalization | |
| dc.title | A Parametric Fitch-Style Modal Lambda Calculus | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master's Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |