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 system which describes polymorphic well-typings for logic programs while respecting the main properties that make types useful and semantically sound. We now tackle the question of automatically producing a well typing for a logic program. We concentrated first on the implementation of a new type inference algorithm and its application to several logic programs.
You may also like
Evidential transactions (ETs) provide auditable and composable evidence that serves as a witness or a proof that a transaction has been correctly […]
In this paper we research methods of supercompilation in the context of relational program specialization. We implement a supercompiler for miniKanren with […]
We present an extension of our prior work on certified semantics for core miniKanren, introducing disequality constraints in the language. Semantics is […]
Runtime verification (RV) consists in dynamically checking event traces generated by single runs of a system against a formal specification; such a […]