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: | English |
| Published: |
Association for Computing Machinery,
2021-09-23T19:09:23Z.
|
| Subjects: | |
| Online Access: | Get fulltext |