A Parametric Fitch-Style Modal Lambda Calculus
Examensarbete för masterexamen
Computer science – algorithms, languages and logic (MPALG), MSc
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  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.
Necessity , modality , parametric , Fitch , modal , lambda calculus , normalization