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 条
  • [31] Towards a refinement calculus for object systems
    He, JF
    Liu, ZM
    Li, XS
    FIRST IEEE INTERNATIONAL CONFERENCE ON COGNITIVE INFORMATICS, PROCEEDINGS, 2002, : 69 - 76
  • [32] Fusion and simultaneous execution in the refinement calculus
    Back, RJ
    Butler, M
    ACTA INFORMATICA, 1998, 35 (11) : 921 - 949
  • [33] Local abstraction-refinement for the μ-calculus
    Fecher H.
    Shoham S.
    International Journal on Software Tools for Technology Transfer, 2011, 13 (04) : 289 - 306
  • [34] CRefine: Support for the Circus Refinement Calculus
    Oliveira, M. V. M.
    Gurgel, A. C.
    Castro, C. G.
    SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2008, : 281 - 290
  • [35] The Refinement Calculus of Reactive Systems Toolset
    Iulia Dragomir
    Viorel Preoteasa
    Stavros Tripakis
    International Journal on Software Tools for Technology Transfer, 2020, 22 : 689 - 708
  • [36] Operation refinement and monotonicity in the schema calculus
    Deutsch, M
    Henson, MC
    Reeves, S
    ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, 2003, 2651 : 103 - 126
  • [37] The Refinement Calculus of Reactive Systems Toolset
    Dragomir, Iulia
    Preoteasa, Viorel
    Tripakis, Stavros
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2020, 22 (06) : 689 - 708
  • [38] The Refinement Calculus of Reactive Systems Toolset
    Dragomir, Iulia
    Preoteasa, Viorel
    Tripakis, Stavros
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II, 2018, 10806 : 201 - 208
  • [39] Tool Support for the Circus Refinement Calculus
    Gurgel, A. C.
    de Castro, C. G.
    Oliveira, M. V. M.
    ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, 2008, 5238 : 349 - 349
  • [40] REFINEMENT OF FUNCTIONAL CALCULUS OF CALDERON AND ZYGMUND
    SEELEY, RT
    KONINKLIJKE NEDERLANDSE AKADEMIE VAN WETESCHAPPEN-PROCEEDINGS SERIES A-MATHEMATICAL SCIENCES, 1965, 68 (03): : 521 - &
12345