Cover Image

Internalizing Representation Independence with Univalence

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Angiuli, Carlo, Cavallo, Evan, Mörtberg, Anders, Zeuner, Max
Format:	Preprint
Published:	2020
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Univalent Formalization of Constructive Affine Schemes
by: Zeuner, Max, et al.
Published: (2022)

Automating Boundary Filling in Cubical Type Theories
by: Doré, Maximilian, et al.
Published: (2024)

Univalence without function extensionality
by: Cavallo, Evan, et al.
Published: (2026)

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

A dependently-typed calculus of event telicity and culminativity
by: Kovalev, Pavel, et al.
Published: (2025)

Univalent Foundations of Constructive Algebraic Geometry
by: Zeuner, Max
Published: (2024)

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
by: Ljungström, Axel, et al.
Published: (2023)

Computational Synthetic Cohomology Theory in Homotopy Type Theory
by: Ljungström, Axel, et al.
Published: (2024)

Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
by: Bao, Jialu, et al.
Published: (2024)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
by: Zilberstein, Noam, et al.
Published: (2024)

First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
by: Lohse, Janine, et al.
Published: (2026)

Verifying Functional Correctness Properties At the Level of Java Bytecode
by: Paganoni, Marco, et al.
Published: (2024)

Reasoning About Exceptional Behavior At the Level of Java Bytecode
by: Paganoni, Marco, et al.
Published: (2024)

A Graded Modal Dependent Type Theory with Erasure, Formalized
by: Abel, Andreas, et al.
Published: (2026)

GATlab: Modeling and Programming with Generalized Algebraic Theories
by: Lynch, Owen, et al.
Published: (2024)

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

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

An Intermediate Program Representation for Optimizing Stream-Based Languages
by: Baumeister, Jan, et al.
Published: (2025)

On Small Types in Univalent Foundations
by: de Jong, Tom, et al.
Published: (2021)

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
by: Matsuoka, Satoshi
Published: (2026)

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
by: Carette, TItouan, et al.
Published: (2022)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
by: Barth, Max, et al.
Published: (2025)

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

Derivatives for Containers in Univalent Foundations
by: Joram, Philipp, et al.
Published: (2025)

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

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Compositional theories for host-core languages
by: Trotta, Davide, et al.
Published: (2020)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Crash-Stop Failures in Asynchronous Multiparty Session Types
by: Barwell, Adam D., et al.
Published: (2023)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
by: Kobayashi, Kentaro, et al.
Published: (2025)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
by: Zhang, Cheng, et al.
Published: (2026)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)