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/