scientific article; zbMATH DE number 7756115

DOI10.4230/lipics.types.2019.10MaRDI QIDQ6079241

Nils Anders Danielsson

Publication date: 27 October 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

higher inductive typescubical agda

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

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

Cites Work

• Unnamed Item
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: