Title: Eliminating dependent pattern matching without K (talk)
Authors: Cockx, Jesper # ×
Issue Date: 22-May-2014
Conference: Agda Implementors’ Meeting edition:XIX location:Paris date:22-28 May 2014
Abstract: Dependent pattern matching is a fundamental technique for writing Agda code, but by default it implies the K axiom, making it incompatible with homotopy type theory. The —without-K flag imposes a syntactic check for definitions that rely on K, however so far it lacked a formal correctness proof. In this talk, I propose a new specification for —without-K that works by limiting the unification algorithm used for case splitting. It is strictly more liberal than the current specification, particularly when pattern matching on parametrized datatypes, and at the same time it solves a currently open problem with the syntactic check. More importantly, it allows a translation of definitions by pattern matching to eliminators in the style of Goguen et al. (2006) without relying on the K axiom, thus proving its correctness. So with it, we can finally stop worrying when using pattern matching in HoTT.
Publication status: published
KU Leuven publication type: IMa
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:

There are no files associated with this item.


All items in Lirias are protected by copyright, with all rights reserved.