Verification on higher-order recursive schemes

Prelegent(ci)

Igor Walukiewicz

Afiliacja

LaBRI, Bordeaux

Termin

25 kwietnia 2012 14:15

Pokój

p. 5870

Seminarium

Seminarium „Teoria automatów”

---

We propose a new approach to analysing higher-order recursive
schemes. Higher-order recursive schemes were introduced by Damm in the
80-ties as a respelling of simply-typed lambda calculus with fixpoints
(lambda-Y). In this century the interest in higher-order schemes has
been renewed by the discovery by Knapik, Niwinski and Urzyczyn of the
equivalence between higher-order pushdown automata of order n and
schemes of order n satisfying a syntactic constraint called
safety. Later Ong has proved that trees generated by recursive schemes
without safety restriction have decidable monadic second-order theory.

We will present two new approaches to annalysing recursive
schemes. The first one uses stadandard models of lambda-Y. The second
uses evaluation  model called Krivine machine.  Both methods are quite
standard in the lambda-calculus community, but have not yet been
applied to verification problems. We will show that they are extremely
well adapted to the task.

---