Embedding the refinement calculus in Coq
Publication date
2018-10-15
Authors
Alpuim, Joao
Swierstra, W.S.
Editors
Advisors
Supervisors
Document Type
Article
Metadata
Show full item recordCollections
License
taverne
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.
Keywords
Coq, Dependent types, Free monad, Predicate transformers, Refinement calculus, Taverne
Citation
Alpuim, J & Swierstra, W 2018, 'Embedding the refinement calculus in Coq', Science of Computer Programming, vol. 164, pp. 37-48. https://doi.org/10.1016/j.scico.2017.04.003