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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:20 - 16:30
Type TheoryResearch Papers at Aurora Borealis
Chair(s): Jennifer Paykin Galois, Inc.
15:20
23m
Talk
Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq
Research Papers
15:43
23m
Talk
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypesDistinguished Paper
Research Papers
Andrea Vezzosi Chalmers University of Technology, Anders Mörtberg Department of Mathematics, Stockholm University, Andreas Abel Gothenburg University
16:06
23m
Talk
Approximate Normalization for Gradual Dependent Types
Research Papers
Joseph Eremondi University of British Columbia, Éric Tanter University of Chile & Inria Paris, Ronald Garcia University of British Columbia
Pre-print