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 条
  • [41] Reasoning about pointers in refinement calculus
    Back, RJ
    Fan, XC
    Preoteasa, V
    ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2003, : 425 - 434
  • [42] rCOS: A refinement calculus of object systems
    He Jifeng
    Li, Xiaoshan
    Liu, Zhiming
    THEORETICAL COMPUTER SCIENCE, 2006, 365 (1-2) : 109 - 142
  • [43] Embedding calculus and grope cobordism of knots
    Kosanovic, Danica
    ADVANCES IN MATHEMATICS, 2024, 451
  • [44] Coloured Petri net refinement specification and correctness proof with Coq
    Choppy, Christine
    Mayero, Micaela
    Petrucci, Laure
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (03) : 195 - 202
  • [45] Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
    Forster, Yannick
    Smolka, Gert
    INTERACTIVE THEOREM PROVING (ITP 2017), 2017, 10499 : 189 - 206
  • [46] Constructive data refinement in typed lambda calculus
    Honsell, F
    Longley, J
    Sannella, D
    Tarlecki, A
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2000, 1784 : 161 - 176
  • [47] Refinement Calculus as a Theory of Contracts (Invited Paper)
    Back, Ralph-Johan
    UNIFYING THEORIES OF PROGRAMMING, 2010, 5713 : 1 - 1
  • [48] Using refinement calculus techniques to prove linearizability
    Jonsson, Bengt
    FORMAL ASPECTS OF COMPUTING, 2012, 24 (4-6) : 537 - 554
  • [49] Safe modification of pointer programs in refinement calculus
    Nishimura, Susumu
    MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, 2008, 5133 : 284 - 304
  • [50] Practical data refinement for the Z schema calculus
    Groves, L
    ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, 2005, 3455 : 393 - 413
12345