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.

Conference Day
Tue 9 Jan

Displayed time zone: Tijuana, Baja California change

16:00 - 17:30
Session 2-3PEPM at Crocker
Chair(s): Barry JayUniversity of Technology Sydney
16:00
10m
Talk
Towards Language-independent Code Synthesis (Poster/Demo Talk)
PEPM
Jan BessaiTechnical University Dortmund, Boris DüdderUniversity of Copenhagen, George HeinemanWorcester Polytechnic Institute, Jakob RehofTechnical University Dortmund
File Attached
16:10
10m
Talk
Dataflow Metaprogramming (Poster/Demo Talk)
PEPM
Dominic Duggan, Jianhua YaoStevens Institute of Technology
16:20
10m
Talk
An Approach to Generating Text-Based IDEs with Syntax Completion (Poster/Demo Talk)
PEPM
Isao SasanoShibaura Institute of Technology
16:30
10m
Talk
Modular Macros (Poster/Demo Talk)
PEPM
Olivier Nicole, Leo WhiteJane Street, Jeremy YallopUniversity of Cambridge, UK
File Attached
16:40
10m
Talk
Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)
PEPM
File Attached
16:50
40m
Other
Posters/Demos
PEPM