Tue 9 Jan 2018 16:40 - 16:50 at Crocker - Session 2-3 Chair(s): Barry Jay

Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and well-founded recursion and derives useful proof principles for demonstrating properties about them. In this presentation we give an overview of several components of Equations through the help of an example that will serve as a main thread during the session. First of all, we describe the splitting tree, the intermediate data structure used to represent a function defined by Equations. We also explain how recursive definitions are handled by Equations. Finally, we present a mostly independent module that allows to simplify equalities generated to perform dependent pattern-matching on a variable.

Tue 9 Jan

PEPM-2018
16:00 - 17:30: PEPM 2018 - Session 2-3 at Crocker
Chair(s): Barry JayUniversity of Technology Sydney
PEPM-2018151551000000016:00 - 16:10
Talk
Jan BessaiTechnical University Dortmund, Boris DüdderUniversity of Copenhagen, George HeinemanWorcester Polytechnic Institute, Jakob RehofTechnical University Dortmund
File Attached
PEPM-2018151551060000016:10 - 16:20
Talk
Dominic Duggan, Jianhua YaoStevens Institute of Technology
PEPM-2018151551120000016:20 - 16:30
Talk
Isao SasanoShibaura Institute of Technology
PEPM-2018151551180000016:30 - 16:40
Talk
Olivier Nicole, Leo WhiteJane Street, Jeremy YallopUniversity of Cambridge, UK
File Attached
PEPM-2018151551240000016:40 - 16:50
Talk
File Attached
PEPM-2018151551300000016:50 - 17:30
Other