Parametricity and refinements for effective algebra in Coq

Speaker: Maxime Dénès , University of Pennsylvania

Date: Tuesday, April 08, 2014

Time: 2:00 PM to 3:00 PM Note: all times are in the Eastern Time Zone

Refreshments: 2:00 PM

Public: Yes

Location: 32-G882

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL: http://www.maximedenes.fr/

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu, pl@lists.csail.mit.edu

Reminder Subject: TALK: Parametricity and refinements for effective algebra in Coq

Proof assistants like Coq provide a unified framework to describe the implementation of algorithms and their proofs of correctness. However, proof-oriented aspects are often in tension with the efficiency of representations. To work around this issue, we design a Coq framework based on data refinements. The idea is to prove correctness on a convenient, proof-oriented, instance and then transport this proof on a executable, more efficient instance. We automate most of this transport by reusing some ideas from the parametricity theorem.

Finally, we will show how we applied this approach to concrete examples, scaling up to a library of verified algorithms from computer algebra (mainly linear algebra and homology). Such algorithms are interesting use cases because they make the tension between property-oriented and computation-oriented descriptions particularly salient.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Adam Chlipala Email at Wednesday, March 26, 2014 at 10:52 AM.