Cubical Agda: A dependently typed programming language with univalence and higher inductive types

DOI10.1017/S0956796821000034OpenAlexW3141612224MaRDI QIDQ5016211

Andreas Abel, Andrea Vezzosi, Anders Mörtberg

Publication date: 13 December 2021

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796821000034

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (16)

Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ Martin Hofmann’s contributions to type theory: Groupoids and univalence ⋮ Unnamed Item ⋮ Quotients by Idempotent Functions in Cedille ⋮ Subtyping without reduction ⋮ Type-theoretic approaches to ordinals ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Higher order functions and Brouwer’s thesis ⋮ Extensional equality preservation and verified generic programming ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• Coq
• Agda
• Lean
• Idris
• cubicaltt
• RedPRL
• HoTTSQL
• Cubical agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isomorphism is equality
• The simplicial model of univalent foundations (after Voevodsky)
• Guarded cubical type theory
• Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
• Copatterns
• Refinements for Free!
• A type theory for synthetic $\infty$-categories
• The Lean Theorem Prover (System Description)
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A Cubical Approach to Synthetic Homotopy Theory
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Elaborating dependent (co)pattern matching: No pattern left behind
• On Higher Inductive Types in Cubical Type Theory
• The Integers as a Higher Inductive Type
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Non-wellfounded trees in Homotopy Type Theory
• The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory
• Homotopical patch theory
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Homotopy Type Theory: Univalent Foundations of Mathematics
• An experimental library of formalized Mathematics based on the univalent foundations

This page was built for publication: Cubical Agda: A dependently typed programming language with univalence and higher inductive types