A Parametric Fitch-Style Modal Lambda Calculus
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2023
Författare
Forsman, Axel
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Necessity , modality , parametric , Fitch , modal , lambda calculus , normalization