Certified Semantics for Disequality (miniKanren 2020) - ICFP 2020

Write a Blog >>

Thu 20 - Fri 28 August 2020

Who

Dmitry Rozplokhas, Dmitri Boulytchev

Track

miniKanren 2020

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Thu 27 Aug 2020 13:10 - 13:30 at miniKanren - Morning Session Chair(s): Joseph P. Near, Gregory Rosenblatt

Abstract

We present an extension of our prior work on certified semantics for core miniKanren, introducing disequality constraints in the language. Semantics is parameterized by an exact definition of constraint stores, allowing us to cover different implementations, and we provide a list of sufficient conditions on this definition for search completeness. We also give two examples of concrete implementations of constraint stores that satisfy those sufficient conditions. The description and proofs are partially certified in Coq and a correct-by-construction interpreter is extracted.

Link to Publication

http://minikanren.org/workshop/2020/minikanren-2020-paper6.pdf

Dmitry Rozplokhas

Higher School of Economics

Dmitri Boulytchev

St. Petersburg State University, St. Petersburg, Russia

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Thu 27 Aug
Displayed time zone: Eastern Time (US & Canada) change

	11:30 - 13:30	Morning SessionminiKanren at miniKanren Chair(s): Joseph P. Near University of Vermont, Gregory Rosenblatt University of Alabama at Birmingham, USA

	11:30 20m Talk		On Fair Relational Conjunction miniKanren Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia Link to publication
	11:50 20m Talk		An Empirical Study of Partial Deduction for miniKanren miniKanren Ekaterina Verbitskaia JetBrains, Daniil Berezun JetBrains, Russia, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia Link to publication
	12:10 20m Talk		MicroKanren in J: an Embedding of the Relational Paradigm in an Array Language with Rank-Polymorphic Unification miniKanren Raoul Schorer Geneva University Hospitals Link to publication
	12:30 20m Talk		λKanren: Higher-order Logic Programming with Shallow Embedding miniKanren Weixi Ma Indiana University, Kuang-Chen Lu Indiana University Bloomington, Daniel P. Friedman Indiana University, USA Link to publication
	12:50 20m Talk		Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System miniKanren Marco Maggesi Università di Firenze, Massimo Nocentini Università di Firenze Link to publication
	13:10 20m Talk		Certified Semantics for Disequality miniKanren Dmitry Rozplokhas Higher School of Economics, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia Link to publication