Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Wed 2 Dec 2020 17:30 - 18:00 at online - Semantics Chair(s): Florian Rabe

We present a formal study of semantics for relational programming language miniKanren. First, we formulate denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models the distinctive feature of miniKanren implementation — interleaving, — 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.

Wed 2 Dec
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

17:30 - 19:00
SemanticsResearch Papers at online
Chair(s): Florian Rabe University of Erlangen
17:30
30m
Talk
Certified Semantics for Relational Programming
Research Papers
Dmitry RozplokhasHigher School of Economics and JetBrains Research, Russia, Andrey VyatkinSaint Petersburg State University, Russia, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research
18:00
30m
Talk
An Abstract Machine for Strong Call by Value
Research Papers
Malgorzata BiernackaUniversity of Wroclaw, Dariusz BiernackiUniversity of Wrocław, Witold CharatonikInstitute of Computer Science, University of Wroclaw, Tomasz DrabInstitute of Computer Science, University of Wroclaw
18:30
30m
Talk
Algebraic and coalgebraic perspectives on interaction laws
Research Papers
Tarmo UustaluReykjavik University, Niels VoorneveldTallinn University of Technology