Date: Sep 3, 2015 11:00am - 12:00pm
Location: GDC 2.104
Talk Audience: UTCS Faculty, Grads, Other Interested Parties
Host: William Cook
In this talk, I present Fiat, a framework for the deductive synthesis of abstract datatypes (ADTs) built entirely within the Coq proof assistant. Fiat supports a high degree of automation by means of meta-programming tactics which help users interactively derive efficient implementations of ADTs from high-level, declarative specifications. Every derivation leaves a proof trail, checkable by the normal Coq kernel, justifying the correctness of the derived implementation. Thanks to this proof trail, users can incorporate their own insights into a derivation while maintaining a high degree of confidence in the correctness of the synthesized implementation.
I will demo Fiat’s domain-specific synthesis library for synthesizing ADTs with SQL-like... Read more