Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq
Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.
Mon 19 Aug
|15:20 - 15:43|
|15:43 - 16:06|
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypesDistinguished Paper
|16:06 - 16:30|
Joseph EremondiUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris, Ronald GarciaUniversity of British ColumbiaPre-print