Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › Рецензирование
Certified Semantics for Relational Programming. / Rozplokhas, Dmitry; Vyatkin, Andrey; Boulytchev, Dmitry.
Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. ред. / Bruno C. Oliveira. Springer Nature, 2020. стр. 167-185 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 12470 LNCS).Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › Рецензирование
}
TY - GEN
T1 - Certified Semantics for Relational Programming
AU - Rozplokhas, Dmitry
AU - Vyatkin, Andrey
AU - Boulytchev, Dmitry
N1 - Funding Information: The reported study was funded by RFBR, project number 18-01-00380. 1A detailed Prolog-to-miniKanren comparison can be found here: http:// minikanren.org/minikanren-and-prolog.html. Publisher Copyright: © 2020, Springer Nature Switzerland AG. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85097643219&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-64437-6_9
DO - 10.1007/978-3-030-64437-6_9
M3 - Conference contribution
AN - SCOPUS:85097643219
SN - 9783030644369
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 185
BT - Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings
A2 - Oliveira, Bruno C.
PB - Springer Nature
T2 - 18th Asian Symposium on Programming Languages and Systems, APLAS 2020
Y2 - 30 November 2020 through 2 December 2020
ER -
ID: 76606691