A logical framework for reasoning about logical specifications
John Hannan, Alwen Tiu · 2004
We present a new logic, Linc, which is designed to be used as a framework for specifying and reasoning about operational semantics. Linc is an extension of first-order intuitionistic logic with a proof theoretic notion of definitions, induction and co-induction, and a new quantifier ∇. Definitions can be seen as expressing fixed point equations, and the least and greatest solutions for the fixed point equations give rise to the induction and co-induction proof principles. The quantifier ∇ focuses on the intensional reading of ∀ and is used to reason about over λ-terms which makes it possible to reason about encodings involving co-exist within the same logic, allowing for expressing proofs involving induction and co-induction on both first-order and higher-order encodings of operational semantics. We prove the cut-elimination and the consistency results for Linc, extending the reducibility technique due to Tait and Martin-Lof. We illustrate the applications of Linc in a number of areas, ranging from data structures, expressive power of the full logic is demonstrated in the encoding of π-calculus, where we show that the notion of names in the calculus can naturally be interpreted in the quantification theory of Linc.