Contributions
13 posts
We discuss the influences of structural proof theory on logic programming and vice versa. Attachments Abstract Dale Miller (87 kB)
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 […]
While many logic programming systems like miniKanren are highly expressive, they suffer from long and unpredictable running times. The challenge comes from the search algorithm being usually an uninformed search. Through the domain of program synthesis we show that it possible to greatly speedup this search by guiding it using […]
We report on ongoing work on introducing a mechanism for private types in a higher-order logic programming language such as λProlog. Attachments Abstract Marco Maggesi and Enrico Tassi (124 kB)
We present an approach to pattern matching code generation based on application of relational programming and, in particular, relational interpreters. Attachments Abstract Dmitrii Kosarev and Dmitry Boulytchev (130 kB)
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. […]
Internet routing is the process of selecting paths across the Internet to connect the communicating hosts, it is unique in that path selection is jointly determined by a network of independently operated networks, known as domains or Autonomous Systems (ASes), that interconnect to form the Internet. In fact, the present […]
In this paper we research methods of supercompilation in the context of relational program specialization. We implement a supercompiler for miniKanren with different unfolding strategies and compare them. Attachments Abstract Maria Kuklina and Ekaterina Verbitskaia (124 kB)
Type systems are a powerful tool in modern programming languages. We argue that, to be successfully adopted by the logic programming community, the first step is to design a type system that is able to catch obvious and relevant errors at compile-time. To do so, we defined a new type […]
We present a binding-time analysis algorithm for miniKanren. It is capable to determine the order in which names within a program are bound and can be used to facilitate specialization and as a step of conversion into a functional language. Attachments Abstract Ekaterina Verbitskaia, Irina Artemeva and Daniil Berezun (49 […]
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 […]
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. Attachments Abstract Olivier Hermant and James Lipton (129 kB)