Normalization for Fitch-Style Modal Calculi
summary
Claims a modular semantic normalization procedure for Fitch-style modal lambda calculi: it builds Normalization by Evaluation models from a single possible-world interface, instantiates worlds as contexts and modal accessibility as the context-extension relation, and yields a concrete normalizer that handles K, T and 4 axioms and both beta- and eta-equivalence. The development is fully Agda mechanization, so the paper provides an algorithmic NbE implementation and a recipe to add or mix modal operations without redoing ad hoc syntactic lemmas.
AI-written summary · about