Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery
2014
|
| Online Access: | http://hdl.handle.net/1721.1/91993 https://orcid.org/0000-0002-9427-4891 https://orcid.org/0000-0001-7085-9417 https://orcid.org/0000-0002-1900-3901 |
| _version_ | 1811093139596771328 |
|---|---|
| author | Delaware, Benjamin James Pit-Claudel, Clement F. Gross, Jason S. Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Delaware, Benjamin James Pit-Claudel, Clement F. Gross, Jason S. Chlipala, Adam |
| author_sort | Delaware, Benjamin James |
| collection | MIT |
| description | We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures--abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a suite of tactics for automating the refinement of specifications into efficient, correct- by-construction OCaml code. Using these tactics, a programmer can generate such an implementation completely automatically by only specifying the equivalent of SQL indexes, data structures capturing useful views of the abstract data. Throughout we speculate on the new programming modularity possibilities enabled by an automated refinement system with proved-correct rules. “Every block of stone has a statue inside it and it is the task of the sculptor to discover it.”--Michelangelo |
| first_indexed | 2024-09-23T15:40:20Z |
| format | Article |
| id | mit-1721.1/91993 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T15:40:20Z |
| publishDate | 2014 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | mit-1721.1/919932021-09-10T15:55:27Z Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant Delaware, Benjamin James Pit-Claudel, Clement F. Gross, Jason S. Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Chlipala, Adam Delaware, Benjamin James Pit-Claudel, Clement F. Gross, Jason S. Chlipala, Adam We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures--abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a suite of tactics for automating the refinement of specifications into efficient, correct- by-construction OCaml code. Using these tactics, a programmer can generate such an implementation completely automatically by only specifying the equivalent of SQL indexes, data structures capturing useful views of the abstract data. Throughout we speculate on the new programming modularity possibilities enabled by an automated refinement system with proved-correct rules. “Every block of stone has a statue inside it and it is the task of the sculptor to discover it.”--Michelangelo National Science Foundation (U.S.) (NSF grant CCF-1253229) United States. Defense Advanced Research Projects Agency (DARPA, agreement number FA8750-12-2- 0293) 2014-12-02T19:57:35Z 2014-12-02T19:57:35Z 2015-01 Article http://dl.acm.org/citation.cfm?id=2676726 978-1-4503-3300-9 http://hdl.handle.net/1721.1/91993 Delaware, Benjamin, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. "Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant." POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Tata Institute of Fundamental Research, Mumbai, India, January 12-18, 2015. https://orcid.org/0000-0002-9427-4891 https://orcid.org/0000-0001-7085-9417 https://orcid.org/0000-0002-1900-3901 en_US http://popl.mpi-sws.org/2015/program.html Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery Chlipala |
| spellingShingle | Delaware, Benjamin James Pit-Claudel, Clement F. Gross, Jason S. Chlipala, Adam Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant |
| title | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant |
| title_full | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant |
| title_fullStr | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant |
| title_full_unstemmed | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant |
| title_short | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant |
| title_sort | fiat deductive synthesis of abstract data types in a proof assistant |
| url | http://hdl.handle.net/1721.1/91993 https://orcid.org/0000-0002-9427-4891 https://orcid.org/0000-0001-7085-9417 https://orcid.org/0000-0002-1900-3901 |
| work_keys_str_mv | AT delawarebenjaminjames fiatdeductivesynthesisofabstractdatatypesinaproofassistant AT pitclaudelclementf fiatdeductivesynthesisofabstractdatatypesinaproofassistant AT grossjasons fiatdeductivesynthesisofabstractdatatypesinaproofassistant AT chlipalaadam fiatdeductivesynthesisofabstractdatatypesinaproofassistant |