FICS 2010 Invited Talks
Structures
defined by higher-order recursion schemes
Higher-order
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.
pdf
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.
pdf
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
computational systems.
pdf
Back to the FICS home page.
Luigi Santocanale
Dernière mise à jour : Tue Aug 31 2010, 11:13:15