Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Induction and Co-induction in Sequent Calculus
Authors: Alberto Momigliano ; Alwen Tiu
Date:Feb 2004
Publication Type:Conference Paper Publication Status:Published
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 based on a proof theoretic notion of definition, following on work by Schroeder-Heister, Girard, and McDowell and Miller. Definitions are essentially stratified logic programs. The left and right rules for defined atoms treat the definitions as defining fixed points. The use of definitions also makes it possible to reason intensionally about syntax, in particular enforcing free equality via unification. The full system thus allows inductive and co-inductive proofs involving higher-order abstract syntax. We extend earlier work by allowing induction and co-induction on general definitions and show that cut-elimination holds for this extension. We present some examples involving lists and simulation in the lazy lambda-calculus. Two prototype implementations are available: one via the Hybrid system implemented on top of Isabelle/HOL and the other in the BLinc system implemented on top of lambdaProlog.
Links To Paper
1st Link
Bibtex format
author = { Alberto Momigliano and Alwen Tiu },
title = {Induction and Co-induction in Sequent Calculus},
book title = {},
publisher = {Springer},
year = 2004,
month = {Feb},
doi = {10.1007/b98246},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh