:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Aagaard, Frederik Lerbjerg, Kristensen, Magnus Baunsgaard, Gratzer, Daniel, Birkedal, Lars
Format:	Preprint
Published:	2022
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2203.13000
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A denotationally-based program logic for higher-order store
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2023)

Normalization for multimodal type theory
by: Gratzer, Daniel
Published: (2023)

Controlling unfolding in type theory
by: Gratzer, Daniel, et al.
Published: (2022)

The $\infty$-category of $\infty$-categories in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2026)

Strict universes for Grothendieck topoi
by: Gratzer, Daniel, et al.
Published: (2022)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
by: Gratzer, Daniel, et al.
Published: (2024)

Eliminating reversals from cubical type theories
by: Cavallo, Evan, et al.
Published: (2026)

Normal forms in cubical type theory
by: Huang, Xu
Published: (2026)

Yet another cubical type theory, but via a semantic approach
by: Kapulkin, Chris, et al.
Published: (2025)

Semantics of multimodal adjoint type theory
by: Shulman, Michael
Published: (2023)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
by: de Medeiros, Markus, et al.
Published: (2026)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

Almost-Sure Termination by Guarded Refinement
by: Gregersen, Simon Oddershede, et al.
Published: (2024)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
by: de Jong, Tom, et al.
Published: (2026)

The Yoneda embedding in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

Directed univalence in simplicial homotopy type theory
by: Gratzer, Daniel, et al.
Published: (2024)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

The equivariant model structure on cartesian cubical sets
by: Awodey, Steve, et al.
Published: (2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
by: Aguirre, Alejandro, et al.
Published: (2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Generic bidirectional typing for dependent type theories
by: Felicissimo, Thiago
Published: (2023)

Homotopy type theory as a language for diagrams of $\infty$-logoses
by: Uemura, Taichi
Published: (2022)

Formalizing two-level type theory with cofibrant exo-nat
by: Uskuplu, Elif
Published: (2023)

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
by: Spadetto, Matteo
Published: (2023)

Directed type theory, with a twist
by: Rivera, Fernando Rafael Chu, et al.
Published: (2026)

Context-Dependent Effects and Concurrency in Guarded Interaction Trees
by: Stepanenko, Sergei, et al.
Published: (2025)

Compositional pre-processing for automated reasoning in dependent type theory
by: Blot, Valentin, et al.
Published: (2022)

Classifying covering types in homotopy type theory
by: Mimram, Samuel, et al.
Published: (2025)

Central H-spaces and banded types
by: Buchholtz, Ulrik, et al.
Published: (2023)

Bringing closure to theory combination properties
by: Toledo, Guilherme V., et al.
Published: (2026)

Undecidability of theories of semirings with fixed points
by: Das, Anupam, et al.
Published: (2025)

Encoding call-by-push-value in the pi-calculus
by: Bennetzen, Benjamin, et al.
Published: (2025)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory
by: Stassen, Philipp Jan Andries, et al.
Published: (2024)

Strong negation in the theory of computable functionals TCF
by: Köpp, Nils, et al.
Published: (2022)

On proving consistency of equational theories in Bounded Arithmetic
by: Beckmann, Arnold, et al.
Published: (2022)

Being polite is not enough (and other limits of theory combination)
by: Toledo, Guilherme V., et al.
Published: (2025)