Abstrakt
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 fullblown 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.
Originalsprog  Engelsk 

Artikelnummer  87 
Tidsskrift  Proceedings of the ACM on Programming Languages 
Vol/bind  3 
Udgave nummer  ICFP 
Sider (fratil)  87:187:29 
Antal sider  29 
DOI  
Status  Udgivet  aug. 2019 
Begivenhed  International Conference on Functional Programming (IFCP 2019)  Hotel Scandic Berlin Potsdamer Platz, Berlin, Tyskland Varighed: 18 aug. 2019 → 23 aug. 2019 https://icfp19.sigplan.org/home 
Konference
Konference  International Conference on Functional Programming (IFCP 2019) 

Lokation  Hotel Scandic Berlin Potsdamer Platz 
Land/Område  Tyskland 
By  Berlin 
Periode  18/08/2019 → 23/08/2019 
Internetadresse 
Fingeraftryk
Dyk ned i forskningsemnerne om 'Cubical agda: a dependently typed programming language with univalence and higher inductive types'. Sammen danner de et unikt fingeraftryk.Priser

ICFP'19 Distinguished Paper Award
Vezzosi, Andrea (Modtager), aug. 2019
Pris: Priser, stipendier, udnævnelser