Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12167).
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Book |
| Language: | English |
| Published: |
Springer International Publishing
2021
|
| Online Access: | https://hdl.handle.net/1721.1/131096.2 |
| _version_ | 1811080104318599168 |
|---|---|
| author | Pit-Claudel, Clément Wang, Peng Delaware, Benjamin 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 Pit-Claudel, Clément Wang, Peng Delaware, Benjamin Gross, Jason S. Chlipala, Adam |
| author_sort | Pit-Claudel, Clément |
| collection | MIT |
| description | Part of the Lecture Notes in Computer Science book series (LNCS, volume 12167). |
| first_indexed | 2024-09-23T11:25:53Z |
| format | Book |
| id | mit-1721.1/131096.2 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T11:25:53Z |
| publishDate | 2021 |
| publisher | Springer International Publishing |
| record_format | dspace |
| spelling | mit-1721.1/131096.22021-09-23T18:03:11Z Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs Pit-Claudel, Clément Wang, Peng Delaware, Benjamin Gross, Jason S. Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Part of the Lecture Notes in Computer Science book series (LNCS, volume 12167). We present an original approach to sound program extraction in a proof assistant, using syntax-driven automation to derive correct-by-construction imperative programs from nondeterministic functional source code. Our approach does not require committing to a single inflexible compilation strategy and instead makes it straightforward to create domain-specific code translators. In addition to a small set of core definitions, our framework is a large, user-extensible collection of compilation rules each phrased to handle specific language constructs, code patterns, or data manipulations. By mixing and matching these pieces of logic, users can easily tailor extraction to their own domains and programs, getting maximum performance and ensuring correctness of the resulting assembly code. Using this approach, we complete the first proof-generating pipeline that goes automatically from high-level specifications to assembly code. In our main case study, the original specifications are phrased to resemble SQL-style queries, while the final assembly code does manual memory management, calls out to foreign data structures and functions, and is suitable to deploy on resource-constrained platforms. The pipeline runs entirely within the Coq proof assistant, leading to final, linked assembly code with overall full-functional-correctness proofs in separation logic. NSF (Grants CCF-1512611 and CCF-1521584) DARPA (Contract FA8750-16-C-0007) 2021-09-23T18:00:49Z 2021-07-14T18:20:16Z 2021-09-23T18:00:49Z 2020-06 2021-07-12T18:08:56Z Book http://purl.org/eprint/type/ConferencePaper 0302-9743 1611-3349 https://hdl.handle.net/1721.1/131096.2 Pit-Claudel, Clément et al. "Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs." IJCAR: International Joint Conference on Automated Reasoning, 12167, Springer International Publishing, 2020, 119-137. © 2020 Springer Nature Switzerland en http://dx.doi.org/10.1007/978-3-030-51054-1_7 IJCAR: International Joint Conference on Automated Reasoning Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/octet-stream Springer International Publishing Prof. Chlipala via Phoebe Ayers |
| spellingShingle | Pit-Claudel, Clément Wang, Peng Delaware, Benjamin Gross, Jason S. Chlipala, Adam Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| title | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| title_full | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| title_fullStr | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| title_full_unstemmed | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| title_short | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs |
| title_sort | extensible extraction of efficient imperative programs with foreign functions manually managed memory and proofs |
| url | https://hdl.handle.net/1721.1/131096.2 |
| work_keys_str_mv | AT pitclaudelclement extensibleextractionofefficientimperativeprogramswithforeignfunctionsmanuallymanagedmemoryandproofs AT wangpeng extensibleextractionofefficientimperativeprogramswithforeignfunctionsmanuallymanagedmemoryandproofs AT delawarebenjamin extensibleextractionofefficientimperativeprogramswithforeignfunctionsmanuallymanagedmemoryandproofs AT grossjasons extensibleextractionofefficientimperativeprogramswithforeignfunctionsmanuallymanagedmemoryandproofs AT chlipalaadam extensibleextractionofefficientimperativeprogramswithforeignfunctionsmanuallymanagedmemoryandproofs |