Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Stockholm University, Faculty of Science, Department of Mathematics. Carnegie Mellon University, USA.
2019 (English)In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 3, article id 87Article in journal (Refereed) Published
Abstract [en]

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

Place, publisher, year, edition, pages
2019. Vol. 3, article id 87
Keywords [en]
Cubical Type Theory, Univalence, Higher Inductive Types, Dependent Pattern Matching
National Category
Computer Sciences Algebra and Logic
Research subject
Computing Science; Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-179354DOI: 10.1145/3341691OAI: oai:DiVA.org:su-179354DiVA, id: diva2:1395973
Conference
ICFP 2019: International Conference on Functional Programming, Berlin, Germany, 18-23 August, 2019
Note

Winner of Distinguished Paper Award.

Available from: 2020-02-25 Created: 2020-02-25 Last updated: 2020-02-25Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Mörtberg, Anders
By organisation
Department of Mathematics
Computer SciencesAlgebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 2 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf