Iris from the ground up A modular foundation for higher-order concurrent separation logic

被引：240

作者：

Jung, Ralf ^{[1
]}

Krebbers, Robbert ^{[2
]}

Jourdan, Jacques-Henri ^{[1
]}

Bizjak, Ales ^{[3
]}

Birkedal, Lars ^{[3
]}

Dreyer, Derek ^{[1
]}

机构：

[1] MPI SWS, Saarbrucken, Germany

[2] Delft Univ Technol, Delft, Netherlands

[3] Aarhus Univ, Aarhus, Denmark

来源：

JOURNAL OF FUNCTIONAL PROGRAMMING | 2018年 / 28卷

基金：

欧洲研究理事会;

关键词：

VERIFICATION; REFINEMENT; SEMANTICS; MEMORY; STATE; MODEL;

D O I：

10.1017/S0956796818000151

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.

引用

页数：73

共 76 条

[1] SOLVING REFLEXIVE DOMAIN EQUATIONS IN A CATEGORY OF COMPLETE METRIC-SPACES [J].

AMERICA, P ;

RUTTEN, J .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1989, 39 (03) :343-375

[2]

[Anonymous], P ACM PROGR LANG POP

[3]

Appel AW, 2007, CONFERENCE RECORD OF POPL 2007: THE 34TH ACM SIGPLAN SIGACT SYMPOSIUM ON PRINCIPLES OF PROGAMMING LANGUAGES, P109

[4]

Appel Andrew W, 2001, TOPLAS, V23, P657

[5]

Appel Andrew W, 2014, PROGRAM LOGICS CERTI, DOI DOI 10.1017/CBO9781107256552

[6] Foundational proof-carrying code [J].

Appel, AW .

16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, :247-256

[7] PROVING ASSERTIONS ABOUT PARALLEL PROGRAMS [J].

ASHCROFT, EA .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1975, 10 (01) :110-135

[8]

Beringer L, 2014, LECT NOTES COMPUT SC, V8410, P107

[9] First steps in synthetic guarded domain theory: step-indexing in the topos of trees [J].

Birkedal, Lars ;

Mogelberg, Rasmus Ejlers ;

Schwinghammer, Jan ;

Stovring, Kristian .

26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011), 2011, :55-64

[10] The category-theoretic solution of recursive metric-space equations [J].

Birkedal, Lars ;

Stovring, Kristian ;

Thamsborg, Jacob .

THEORETICAL COMPUTER SCIENCE, 2010, 411 (47) :4102-4122

← 1 2 3 4 5 6 7 8 →