FICS 2010 Invited Talks
defined by higher-order recursion schemes
recursion schemes are a typed rewriting system which naturally
generates infinite trees. The main property of these trees is to have
a decidable monadic second-order theory. This field has received a lot
of attention in the last 10 years. We will try to give a survey of
the most recent results.
We start by presenting the connection with collapsible pushdown automata,
an extension of the model of pushdown automaton which has been
shown to define the same infinite trees.
We will then focus our attention on the subfamily of trees defined
by so called safe recursion schemes. This subfamily was historically
the first considered and was recently shown to be a strict subfamily.
We show how the graphs and linear orders naturally associated to these
trees admit elegant alternative characterizations.
Fixed-Point Semantics for Non-Monotonic Formalisms
We examine two successful application domains for
fixed-point theory, namely (non-monotonic) logic programming
and Boolean grammars. We demonstrate that these two areas are
quite close, and as a result interesting ideas from one area
appear to have interesting counterparts in the other one.
Fixed points and proof theory: an extended abstract
We overview some recent work in the proof theory for fixed points and
illustrate how that theory can be used to provide a unified approach to
computation, model checking, and theorem proving. A key theme in this
work is the development of focused proof system that allow for
micro-rules (e.g., sequent calculus introduction rules) to be
organized into macro- rules. Such macro-rules can often be designed to
correspond closely to “steps” or “actions” taken within
Back to the FICS home page.
Dernière mise à jour : Tue Aug 31 2010, 11:13:15