Live Talks – Workshop on Trends, Extensions, Applications and Semantics of Logic Programming

Dmitry Rozplokhas and Dmitry Boulytchev: Certified Semantics for Disequality Constraints

hbasold — Thu, 14 May 2020 12:50:17 +0000

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. We extend our proof of search completeness to this language extension. The description and proofs are certified in Coq and a correct-by-construction interpreter is extracted.

Forum Full Abstract

Attachments

Abstract Dmitry Rozplokhas and Dmitry Boulytchev (127 kB)

Marco Maggesi and Enrico Tassi: Private types in Higher Order Logic Programming

hbasold — Thu, 14 May 2020 12:40:51 +0000

We report on ongoing work on introducing a mechanism for private types in a higher-order logic programming language such as λProlog.

Forum Full Abstract

Attachments

Abstract Marco Maggesi and Enrico Tassi (124 kB)

Vivek Nigam: A Proof Theory for Distributed Evidential Transactions

hbasold — Thu, 14 May 2020 12:36:33 +0000

Evidential transactions (ETs) provide auditable and composable evidence that serves as a witness or a proof that a transaction has been correctly executed by the named parties. For example, for issuing a Visa, an applicant demonstrates, among other evidence, that he has sufficient financial means to visit a foreign country. The form of evidence in ETs has traditionally been unstructured and informal, in the form of paper-based evidence. This paper proposes a formal treatment of evidence based on proof theory. In particular, we investigate the proof theory of Cyberlogic, an assertion logic for ETs, that enables the combination of evidence represented as logical derivations and as digital certificates, i.e., electronic evidence signed by a principal’s secret key. We propose a proof system for Cyberlogic, refining it with further constructions that support a wider range of ETs. We prove that the proof system admits cut-elimination.

Moreover, we propose a sound and complete focused proof system for the refinement of Cyberlogic thus enabling efficient proof-search. Furthermore, we identify a fragment of Cyberlogic, called Cyberlogic Programs, that can be used to efficiently program ETs using a variety of FOL engines. Finally, we propose Proof Certificate format for Cyberlogic Programs inspired by Foundational Proof Certificates as a means to communicate evidence and check its validity.

This is joint work with Giselle Reis, Harald Ruess, Dian Balta, Tewodros Beyene, and Natarajan Shankar.

Forum Full Abstract

Attachments

Abstract Vivek Nigam (91 kB)

Davide Ancona, Luca Franceschini, Angelo Ferrando and Viviana Mascardi: A SWI-Prolog based implementation of RML

hbasold — Thu, 14 May 2020 12:28:06 +0000

Runtime verification (RV) consists in dynamically checking event traces generated by single runs of a system against a formal specification; such a technique can be used after deployment to monitor and properly handle misbehavior.

We report on the implementation of RML, an expressive rewriting-based domain specific language for RV, where from specifications, monitors are automatically generated in SWI-Prolog; the LP paradigm and some advanced features of SWI-Prolog are particularly suited to adopt Prolog as a target language for RML.

Forum Full Abstract

Attachments

Abstract Davide Ancona, Luca Franceschini, Angelo Ferrando and Viviana Mascardi (260 kB)

Olivier Hermant and James Lipton: Eliminating Cuts in HoiC

hbasold — Thu, 14 May 2020 12:21:30 +0000

We discuss the problem of cut elimination in an intuitionistic version of Church’s Type Theory with constraints, a problem that arises in considering executable fragments suitable for logic programming.

Forum Full Abstract

Attachments

Abstract Olivier Hermant and James Lipton (129 kB)