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
Times are displayed in time zone: Tijuana, Baja California change

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