3 papers
cs.LO2025
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…
cs.LO2024
Unifying cubical and multimodal type theory
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer +1
In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical ty…
cs.PL2024
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco +4
Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent…