« zurück

Mutual Exclusion by Interpolation

Kolloquium | 06.05. | 11 Uhr c.t. | Rotunde

The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. We address the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in other areas, such as reasoning about type classes.

Biografie | Jael Kriener

Jael Kriener studierte von 2006 bis 2010 Informatik, Logik und Wissenschaftstheorie in St Andrews. Seit 2010 ist sie Doktorandin der Informatik an der Universität von Kent, Canterbury. Focus ihrer Arbeit sind Programmanalyse, besonders im Bereich der Logik-Programmierung, und die formale Verifikation von Abstract Interpretation in Coq.

Lisa Jungmann