LFCS Seminar: Tuesday 19 July - Nachi Valliappan
Title: Normalization for Fitch-Style Modal Calculi
Abstract
Fitch-style modal lambda calculi feature necessity modalities
in a typed lambda calculus by extending the typing
context with a delimiting “lock” operator. The lock
operator simplifies formulation of typing rules for calculi that
incorporate different modal axioms. These calculi have excellent
computational properties, but each variant demands different,
tedious and seemingly ad hoc treatment to prove meta-theoretic
properties such as normalization. In this work, we identify the
possible-world semantics of Fitch-style calculi and use it to develop
normalization. The possible-world semantics enables a uniform
treatment of Fitch-style calculi by isolating their differences to a
specific parameter that identifies the modal fragment. In this talk,
I’ll present the current results that cover four Fitch-style calculi
and outline next steps to extend this story further.
Paper and mechanization at https://nachivpn.me/k/
LFCS Seminar: Tuesday 19 July - Nachi Valliappan
Venue: IF-G.03