Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
We present a formal study of semantics for the relational programming language miniKanren. First, we formulate a denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models interleaving, the distinctive feature of miniKanren implementation, and prove its soundness and completeness w.r.t. the denotational semantics. Our development is supported by a Coq specification, from which a reference interpreter can be extracted. We also derive from our main result a certified semantics (and a reference interpreter) for SLD resolution with cut and prove its soundness.
Original language | English |
---|---|
Title of host publication | Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings |
Editors | Bruno C. Oliveira |
Publisher | Springer Nature |
Pages | 167-185 |
Number of pages | 19 |
ISBN (Print) | 9783030644369 |
DOIs | |
State | Published - 2020 |
Event | 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 - Fukuoka, Japan Duration: 30 Nov 2020 → 2 Dec 2020 |
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12470 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference | 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 |
---|---|
Country/Territory | Japan |
City | Fukuoka |
Period | 30/11/20 → 2/12/20 |
ID: 76606691