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

Abstract: Fiat is a deductive synthesis framework for deriving correct-by-construction implementations of abstract data types in Coq. The framework uses the representation independence provided by data abstraction to ensure that a derived implementation meets the specification for any possible client. The restriction that an implementation works for every client removes potential optimizations that would be correct for a particular client, however. The proposed talk discuss our ongoing work on formalizing a relaxation of data refinement in order to enable synthesis of implementations that are tailored to a particular client, while preserving the same representation independence guarantees programmers are used to.

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change

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