Certified Abstract Machines for Skeletal Semantics

被引：0

作者：

Ambal, Guillaume ^{[1
]}

Lenglet, Serguei ^{[2
]}

Schmitt, Alan ^{[3
]}

机构：

[1] Univ Rennes, Rennes, France

[2] Univ Lorraine, Nancy, France

[3] INRIA, Rennes, France

来源：

PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22) | 2022年

关键词：

Skeletal Semantics; Operational Semantics; Abstract Machines; Certified Interpretation; FUNCTIONAL CORRESPONDENCE; EVALUATORS;

D O I：

10.1145/3497775.3503676

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Skeletal semantics is a framework to describe semantics of programming languages. We propose an automatic generation of a certified OCaml interpreter for any language written in skeletal semantics. To this end, we introduce two new interpretations, i.e., formal meanings, of skeletal semantics, in the form of non-deterministic and deterministic abstract machines. These machines are derived from the usual big-step interpretation of skeletal semantics using functional correspondence, a standard transformation from big-step evaluators to abstract machines. All these interpretations are formalized in the Coq proof assistant and we certify their soundness. We finally use the extraction from Coq to OCaml to obtain the certified interpreter.

引用

页码：55 / 67

页数：13

共 19 条

[11]

DANVY O, 1990, PROCEEDINGS OF THE 1990 ACM CONFERENCE ON LISP AND FUNCTIONAL PROGRAMMING, P151, DOI 10.1145/91556.91622

[12] Inter-deriving semantic artifacts for object-oriented programming [J].

Danvy, Olivier ;

Johannsen, Jacob .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2010, 76 (05) :302-323

[13]

Jedynak Wojciech, 2013, 15 INT S PRINCIPLES, P25, DOI [10.1145/2505879.2505890, DOI 10.1145/2505879.2505890]

[14]

Leroy Xavier, 2021, OCAML SYSTEM DOCUMEN

[15]

Letouzey P, 2002, LECT NOTES COMPUT SC, V2646, P200

[16] A Systematic Derivation of the STG Machine Verified in Coq [J].

Pirog, Maciej ;

Biernacki, Dariusz .

ACM SIGPLAN NOTICES, 2010, 45 (11) :25-36

[17]

Plotkin G. D., 1975, Theoretical Computer Science, V1, P125, DOI 10.1016/0304-3975(75)90017-1

[18]

Reynolds J.C., 1972, P ACM ANN C BOST MAS, V2, P717, DOI [10.1145/800194.805852, DOI 10.1145/800194.805852]

[19]

The Coq Development Team, 2022, Zenodo, DOI 10.5281/ZENODO.1003420

← 1 2 →