3 papers
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…
math.LO2019
Constructive sheaf models of type theory
Thierry Coquand, Fabian Ruch, Christian Sattler
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive mo…
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…