David Baelde (MdC, LSV, Cachen) will visit the team on Friday 12 Oct 2012. A schedule of his visit is below.
- 10h30 – noon informal discussions focusing on, say, Abella related topics.
- noon-14h lunch
- 14h-15h30 talk by David. Title and abstract below.
- 15h30-17h informal discussions focusing on, say, Bedwyr related topics.
Hopefully we get to speak about various proof theory topics as well during the day. If you want to meet with David about specific things, please let him and I know.
Title: Fixed points, definitions, and parity
I will talk about various proof formalisms dealing with (co)inductive specifications. At the level of formulas, we’ll have definitions on one hand, and fixed point combinators on the other; at the level of proofs, we’ll have (co)induction rules, but also infinite and cyclic proofs that only unfold definitions. These different styles are intuitively related, but I’ve been missing formal results for a long time. I’ll present such formal relationship by bringing in mu-calculus and parity games, showing that they make a lot of sense in sequent calculus, though hard questions remain.
