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 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:20 - 16:30
|Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq|
|Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypesDistinguished Paper|
|Approximate Normalization for Gradual Dependent Types|
Joseph Eremondi University of British Columbia, Éric Tanter University of Chile & Inria Paris, Ronald Garcia University of British ColumbiaPre-print