Embedding the refinement calculus in Coq

被引：2
|
作者：
Alpuim, Joao [1 ]
Swierstra, Wouter [2 ]
机构：
[1] Univ Hong Kong, Hong Kong, Hong Kong, Peoples R China
[2] Univ Utrecht, Utrecht, Netherlands
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2018年 / 164卷
关键词：
Refinement calculus; Coq; Predicate transformers; Free monad; Dependent types;
D O I：
10.1016/j.scico.2017.04.003
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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. (C) 2017 Elsevier B.V. All rights reserved.
引用
收藏
页码：37 / 48
页数：12
相关论文
共 50 条
  • [1] THE REFINEMENT CALCULUS
    WOODCOCK, JCP
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 552 : 80 - 95
  • [2] Embedding the hypersequent calculus in the display calculus
    Ramanayake, Revantha
    JOURNAL OF LOGIC AND COMPUTATION, 2015, 25 (03) : 921 - 942
  • [3] A verified model checker for the modal μ-calculus in Coq
    Sprenger, C
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 167 - 183
  • [4] A refinement calculus for Statecharts
    Scholz, P
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 1998, 1382 : 285 - 301
  • [5] Z AND THE REFINEMENT CALCULUS
    KING, S
    LECTURE NOTES IN COMPUTER SCIENCE, 1990, 428 : 164 - 188
  • [6] A TUTORIAL ON THE REFINEMENT CALCULUS
    WOODCOCK, JCP
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 552 : 79 - 79
  • [7] A Refinement Calculus for Promela
    Sharma, Asankhaya
    2013 18TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 2013, : 75 - 84
  • [8] A refinement calculus for VHDL
    Breuer, PT
    Kloos, CD
    Madrid, NM
    Marin, A
    Sanchez, L
    EURO-DAC '96 - EUROPEAN DESIGN AUTOMATION CONFERENCE WITH EURO-VHDL '96 AND EXHIBITION, PROCEEDINGS, 1996, : 482 - 487
  • [9] Intuitionistic refinement calculus
    Boulme, Sylvain
    Typed Lambda Calculi and Applications, Proceedings, 2007, 4583 : 54 - 69
  • [10] Formalizing Calculus without Limit Theory in Coq
    Fu, Yaoshun
    Yu, Wensheng
    MATHEMATICS, 2021, 9 (12)
12345