Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Mon 19 Aug 2019 15:20 - 15:43 at Aurora Borealis - Type Theory Chair(s): Jennifer Paykin

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

icfp-2019-papers
15:20 - 16:30: Research Papers - Type Theory at Aurora Borealis
Chair(s): Jennifer PaykinGalois, Inc.
icfp-2019-papers15:20 - 15:43
Talk
icfp-2019-papers15:43 - 16:06
Talk
Andrea VezzosiChalmers University of Technology, Anders MörtbergDepartment of Mathematics, Stockholm University, Andreas AbelGothenburg University
icfp-2019-papers16:06 - 16:30
Talk
Joseph EremondiUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris, Ronald GarciaUniversity of British Columbia
Pre-print