FICS 2010 Invited Talks

Arnaud Carayol

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.

Panos Rondogiannis

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.

Dale Miller

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.

Back to the FICS home page.

Luigi Santocanale
Dernière mise à jour : Tue Aug 31 2010, 11:13:15