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 […]
Live Talks
5 posts
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)
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. […]
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)