Showing cs.LOShow all
2 papers · 1 filter
cs.LO2022
Normalization for Fitch-Style Modal Calculi
Nachiappan Valliappan, Fabian Ruch, Carlos Tomé Cortiñas
Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted…
cs.LO2017
Stack Semantics of Type Theory
Thierry Coquand, Bassel Mannaa, Fabian Ruch
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As…