Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CORR

2008

Springer

2008

Springer

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 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 g higher-order abstract syntax. We extended the 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 lazy lists and simulation in lazy -calculus. Two prot...

Related Content

Added |
10 Dec 2010 |

Updated |
10 Dec 2010 |

Type |
Journal |

Year |
2008 |

Where |
CORR |

Authors |
Alwen Tiu, Alberto Momigliano |

Comments (0)