Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System (miniKanren 2020) - ICFP 2020

Write a Blog >>

Thu 20 - Fri 28 August 2020

Who

Marco Maggesi, Massimo Nocentini

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 12:50 - 13:10 at miniKanren - Morning Session Chair(s): Joseph P. Near, Gregory Rosenblatt

Abstract

We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL Light theorem prover. Our tool is at the same time a mechanism for enabling the logic programming style for reasoning and computing in a theorem prover, and a framework for writing logic programs that produce solutions endowed with a formal proof of correctness.

Link to Publication

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

Marco Maggesi

Università di Firenze

Massimo Nocentini

Università di Firenze

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