Title: Induction and Co-induction in Sequent Calculus                     

Abstract:
  Proof search has been used to specify a wide range of computation
systems.  In order to build a framework for reasoning about such
specifications, we make use of a sequent calculus involving induction and
co-induction. These proof principles are actually based on a proof
theoretic notion of definition, following on work by Hallnas and
Schroeder-Heister, Girard, and McDowell and Miller. Definitions are
essentially logic program which are stratified so as to avoid cyclic
calling through negations. The introduction rules for defined atoms treat
the definitions as defining fixed points. The use of definitions also
makes it possible to reason intensionally about syntax since the inference
rules that introduce defined atoms make use of unification and matching,
and both of these operations can be used on first-order terms or
higher-order lambda-terms. The full system thus allows inductive and
co-inductive proofs involving higher-order abstract syntax.

  We extended the earlier work by allowing induction on general
definitions and show that cut-elimination holds for this extension. For
example, proofs about the operational semantics for mini-ML are quite
natural using such induction.

  We extend the logic further by adding co-induction rules. To maintain
consistency, mutually recursive definitions involving induction and
co-induction need to be avoided. Cut-elimination holds thanks to a (fairly
complex) co-reducibility argument.

  A prototype implementation of much of this logic is available in the
Hybrid system implemented on top of Isabelle/HOL and some examples
concerning applicative bisimulation will be demonstrated.

  We consider two additional extensions to this proof system. One is the
use of circular proofs as a way to lazily determine the post-fixpoint to
use in co-inductive proofs. Another is to integrate the nabla quantifier,
a recently proposed quantifier that provides a direct way to deal
internally with the notion of freshness, thereby allowing proofs involving
higher-order abstract syntax to be used in an even more direct way.