More Web Proxy on the site http://driver.im/

research-article

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Authors:

Benjamin Delaware,

Clément Pit-Claudel,

Adam ChlipalaAuthors Info & Claims

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 689 - 700

https://doi.org/10.1145/2676726.2677006

Published: 14 January 2015 Publication History

Abstract

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.

Supplementary Material

MPG File (p689-sidebyside.mpg)

Download
1371.54 MB

References

[1]

Don Batory, Vivek Singhal, Marty Sirkin, and Jeff Thomas. Scalable software libraries. In Proceedings of the 1st ACM SIGSOFT Symposium on Foundations of Software Engineering. ACM, 1993.

Digital Library

[2]

Lee Blaine and Allen Goldberg. DTRE -- a semi-automatic transformation system. In Constructing Programs from Specifications, pages 165--204. Elsevier, 1991.

[3]

Peter Buneman, Leonid Libkin, Dan Suciu, Val Tannen, and Limsoon Wong. Comprehension syntax. SIGMOD Rec., 23(1), March 1994.

Digital Library

[4]

Swarat Chaudhuri, Martin Clochard, and Armando Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2014.

Digital Library

[5]

Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In Certified Programs and Proofs. Springer International Publishing, 2013.

Digital Library

[6]

http://coq.inria.fr/distrib/current/refman/Reference-Manual029.html.

[7]

Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967.

[8]

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, and Mooly Sagiv. Data representation synthesis. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2011.

Digital Library

[9]

J. He, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In Bernard Robinet and Reinhard Wilhelm, editors, ESOP 86, volume 213 of Lecture Notes in Computer Science, pages 187--196. Springer Berlin Heidelberg, 1986.

Digital Library

[10]

C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.

Digital Library

[11]

Barbara Liskov and Stephen Zilles. Programming with abstract data types. In Symposium on Very High Level Languages, New York, NY, USA, 1974. ACM.

Digital Library

[12]

Robert Paige and Fritz Henglein. Mechanical translation of set theoretic problem specifications into efficient RAM code -- a case study. J. Symb. Comput., 4(2):207--232, October 1987.

Digital Library

[13]

Robert Paige and Shaye Koenig. Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst., 4(3), July 1982.

Digital Library

[14]

Dusko Pavlovic, Peter Pepper, and Douglas R. Smith. Formal derivation of concurrent garbage collectors. In Mathematics of Program Construction, pages 353--376. Springer Berlin Heidelberg, 2010.

Digital Library

[15]

Rishabh Singh and Armando Solar-Lezama. Synthesizing data structure manipulations from storyboards. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering. ACM, 2011.

Digital Library

[16]

Douglas R. Smith. KIDS: A semi-automatic program development system. In Client Resources on the Internet, IEEE Multimedia Systems'99, pages 302--307, 1990.

[17]

Douglas R. Smith and Stephen J. Westfold. Synthesis of propositional satisfiability solvers, 2008.

[18]

Armando Solar-Lezama. Program Synthesis by Sketching. PhD thesis, University of California, Berkeley, 2008.

Digital Library

[19]

Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. Sketching concurrent data structures. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2008.

Digital Library

[20]

http://www.kestrel.edu/home/prototypes/specware.html.

[21]

Philip Wadler. Comprehending monads. In Mathematical Structures in Computer Science, pages 61--78, 1992.

Digital Library

Cited By

Cai YHou ZSanan DLuan XLin YSun JDong J(2025)Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement CalculusProceedings of the ACM on Programming Languages10.1145/37049059:POPL(2057-2089)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704905
Arora JLu SJain DXu THoushmand FPhothilimthana PLesani MNarayanan PMurthy KBodik RSabne AMendis C(2025)TensorRight: Automated Verification of Tensor Graph RewritesProceedings of the ACM on Programming Languages10.1145/37048659:POPL(832-863)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704865
Gruetter SFukala VChlipala A(2024)Live Verification in an Interactive Proof AssistantProceedings of the ACM on Programming Languages10.1145/36564398:PLDI(1535-1558)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656439
Show More Cited By

Recommendations

Reconciling enumerative and deductive program synthesis
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate ...
Tops: theory operationalization for program synthesis
Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis

The structured programming literature provides methods and a wealth of heuristic knowledge for guiding the construction of provably correct imperative programs. We investigate these methods and heuristics as a basis for mechanizing program synthesis. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2015

716 pages

ISBN:9781450333009

DOI:10.1145/2676726

General Chair:
Sriram Rajamani
Microsoft Research, India
,
Program Chair:
David Walker
Princeton University, USA

ACM SIGPLAN Notices Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 15 - 17, 2015

Mumbai, India

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

64
Total Citations
View Citations
519
Total Downloads

Downloads (Last 12 months)75
Downloads (Last 6 weeks)11

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cai YHou ZSanan DLuan XLin YSun JDong J(2025)Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement CalculusProceedings of the ACM on Programming Languages10.1145/37049059:POPL(2057-2089)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704905
Arora JLu SJain DXu THoushmand FPhothilimthana PLesani MNarayanan PMurthy KBodik RSabne AMendis C(2025)TensorRight: Automated Verification of Tensor Graph RewritesProceedings of the ACM on Programming Languages10.1145/37048659:POPL(832-863)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704865
Gruetter SFukala VChlipala A(2024)Live Verification in an Interactive Proof AssistantProceedings of the ACM on Programming Languages10.1145/36564398:PLDI(1535-1558)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656439
Liu ABernstein GChlipala ARagan-Kelley J(2024)A Verified Compiler for a Functional Tensor LanguageProceedings of the ACM on Programming Languages10.1145/36563908:PLDI(320-342)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656390
He YZhao PWang XWang Y(2024)VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity ConstraintsProceedings of the ACM on Programming Languages10.1145/36498498:OOPSLA1(1071-1099)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649849
Pailoor SWang YDillig I(2024)Semantic Code Refactoring for Abstract Data TypesProceedings of the ACM on Programming Languages10.1145/36328708:POPL(816-847)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632870
Yang MZhang D(2023)Deep Reinforcement Learning Guided Decision Tree Learning For Program Synthesis2023 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER56733.2023.00112(925-932)Online publication date: Mar-2023
https://doi.org/10.1109/SANER56733.2023.00112
Mishra AJagannathan S(2022)Specification-guided component-based synthesis from effectful librariesProceedings of the ACM on Programming Languages10.1145/35633106:OOPSLA2(616-645)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563310
Chen YWang YGoyal MDong JFeng YDillig I(2022)Synthesis-powered optimization of smart contracts via data type refactoringProceedings of the ACM on Programming Languages10.1145/35633086:OOPSLA2(560-588)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563308
Pit-Claudel CPhilipoom JJamner DErbsen AChlipala AJhala RDillig I(2022)Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level codeProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523706(918-933)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523706
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents