| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 6875166 | Science of Computer Programming | 2018 | 12 Pages |
Abstract
The refinement calculus and type theory are both frameworks that support the specification and verification of programs. This paper presents an embedding of the refinement calculus in the interactive theorem prover Coq, clarifying the relation between the two. As a result, refinement calculations can be performed in Coq, enabling the interactive calculation of formally verified programs from their specification.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
João Alpuim, Wouter Swierstra,