Sat 13 Jan 2018 17:15 - 17:40 at Watercourt A - Semantics and Synthesis Chair(s): Ilya Sergey

The notion of monotonic, or order-preserving, functions is a key notion in programming languages semantics, being used in both logical relations and denotational semantics. In Coq, monotonic functions are also known as Proper functions, because they are usually defined with the Proper typeclass, and they are used for setoid rewriting. Although it is straightforward to define a Coq type for Proper functions, it is onerous and time-consuming to build any non-trivial Proper functions in this type, as the user has to manually write the proofs of monotonicity at every Proper abstraction. Further, rewriting these Proper functions requires rewriting their proofs as well, which can increase the size of expressions dramatically with each rewrite step.

In this talk, ongoing work will be presented that addresses both of these problems. To build Proper functions, a collection of Coq typeclass instances and notations are used to automatically build monotonicity proofs, effectively creating an embedded domain-specific language (EDSL) of Proper functions inside Coq. To rewrite Proper functions, they are first reflected into a Coq inductive datatype that represents Proper functions without requiring monotonicity proofs. This reflection is performed using a second collection of Coq typeclass instances. Because this inductive datatype does not require monotonicity proofs, rewriting becomes orders of magnitude more efficient.

Sat 13 Jan

CoqPL-2018
16:00 - 18:05: - Semantics and Synthesis at Watercourt A
Chair(s): Ilya SergeyUniversity College London
CoqPL-2018151585560000016:00 - 16:25
Talk
Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
File Attached
CoqPL-2018151585710000016:25 - 16:50
Talk
Abhishek AnandCornell University, Greg MorrisettCornell University
File Attached
CoqPL-2018151585860000016:50 - 17:15
Talk
Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University
File Attached
CoqPL-2018151586010000017:15 - 17:40
Talk
Edwin WestbrookGalois, Inc.
File Attached
CoqPL-2018151586160000017:40 - 18:05
Talk
Dan FruminRadboud University, Robbert KrebbersDelft University of Technology
File Attached