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/ Jul 19 2022 16.10 - 17.00 LFCS Seminar: Tuesday 19 July - Nachi Valliappan Speaker: Nachi Valliappan, Chalmers University https://nachivpn.me/ Venue: IF-G.03
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/ Jul 19 2022 16.10 - 17.00 LFCS Seminar: Tuesday 19 July - Nachi Valliappan Speaker: Nachi Valliappan, Chalmers University https://nachivpn.me/ Venue: IF-G.03
Jul 19 2022 16.10 - 17.00 LFCS Seminar: Tuesday 19 July - Nachi Valliappan Speaker: Nachi Valliappan, Chalmers University https://nachivpn.me/
