A Parametric Fitch-Style Modal Lambda Calculus

Publicerad

Författare

Typ

Examensarbete för masterexamen
Master's Thesis

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

Citation

Arkitekt (konstruktör)

Geografisk plats

Byggnad (typ)

Byggår

Modelltyp

Skala

Teknik / material

Index

item.page.endorsement

item.page.review

item.page.supplemented

item.page.referenced