Standard

Certified Semantics for Relational Programming. / Rozplokhas, Dmitry; Vyatkin, Andrey; Boulytchev, Dmitry.

Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. ed. / Bruno C. Oliveira. Springer Nature, 2020. p. 167-185 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12470 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review

Harvard

Rozplokhas, D, Vyatkin, A & Boulytchev, D 2020, Certified Semantics for Relational Programming. in BC Oliveira (ed.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12470 LNCS, Springer Nature, pp. 167-185, 18th Asian Symposium on Programming Languages and Systems, APLAS 2020, Fukuoka, Japan, 30/11/20. https://doi.org/10.1007/978-3-030-64437-6_9

APA

Rozplokhas, D., Vyatkin, A., & Boulytchev, D. (2020). Certified Semantics for Relational Programming. In B. C. Oliveira (Ed.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings (pp. 167-185). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12470 LNCS). Springer Nature. https://doi.org/10.1007/978-3-030-64437-6_9

Vancouver

Rozplokhas D, Vyatkin A, Boulytchev D. Certified Semantics for Relational Programming. In Oliveira BC, editor, Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. Springer Nature. 2020. p. 167-185. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-64437-6_9

Author

Rozplokhas, Dmitry ; Vyatkin, Andrey ; Boulytchev, Dmitry. / Certified Semantics for Relational Programming. Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings. editor / Bruno C. Oliveira. Springer Nature, 2020. pp. 167-185 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

BibTeX

@inproceedings{b29aedc0591d4e3aa8f5f97fd9f6ee05,
title = "Certified Semantics for Relational Programming",
abstract = "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.",
author = "Dmitry Rozplokhas and Andrey Vyatkin and Dmitry Boulytchev",
note = "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: {\textcopyright} 2020, Springer Nature Switzerland AG. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; 18th Asian Symposium on Programming Languages and Systems, APLAS 2020 ; Conference date: 30-11-2020 Through 02-12-2020",
year = "2020",
doi = "10.1007/978-3-030-64437-6_9",
language = "English",
isbn = "9783030644369",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Nature",
pages = "167--185",
editor = "Oliveira, {Bruno C.}",
booktitle = "Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Proceedings",
address = "Germany",

}

RIS

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