A logical framework for reasoning about logical specifications

by 1977- Tiu, Alwen

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 firstorder intuitionistic logic with a proof theoretic notion of definitions, induction and coinduction, 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 encodings of object systems involving abstractions. The logic Linc allows quantification over ?-terms which makes it possible to reason about encodings involving higher-order abstract syntax, a clean and declarative treatment of syntax involving abstraction and substitution. All these features of Linc co-exist within the same logic, allowing for expressing proofs involving induction and coinduction 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-Löf. We illustrate the applications of Linc in a number of areas, ranging from data structures, abstract transition systems, object logic and functional programming. The 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. iv