POPL 2018 (series) / CoqPL 2018 (series) / The Fourth International Workshop on Coq for Programming Languages /
Towards Context-Aware Data Refinement
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.
(KrogmeierKiddDelaware-CoqPL18.pdf) | 515KiB |
(Krogmeier-al-CoqPL18-Slides.pdf) | 925KiB |
Sat 13 Jan Times are displayed in time zone: Tijuana, Baja California change
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 | Phantom Types for Quantum Programs CoqPL Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania File Attached | ||
16:25 - 16:50 Talk | Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL File Attached | ||
16:50 - 17:15 Talk | Towards Context-Aware Data Refinement CoqPL File Attached | ||
17:15 - 17:40 Talk | Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin WestbrookGalois, Inc. File Attached | ||
17:40 - 18:05 Talk | A calculus for logical refinements in separation logic CoqPL File Attached |