A Logical Framework for Reasoning about Logical Specifications
Open Access
- Author:
- Tiu, Alwen Fernanto
- Graduate Program:
- Computer Science and Engineering
- Degree:
- Doctor of Philosophy
- Document Type:
- Dissertation
- Date of Defense:
- March 15, 2004
- Committee Members:
- John Joseph Hannan, Committee Chair/Co-Chair
Mahmut Taylan Kandemir, Committee Member
Padma Raghavan, Committee Member
Stephen George Simpson, Committee Member
Frank Pfenning, Committee Member - Keywords:
- proof theory
operational semantics
co-induction
induction
logical framework
cut-elimination - Abstract:
- 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 nabla. 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 nabla focuses on the intensional reading of the universal quantifier and is used to reason about encodings of object systems involving abstractions. The logic Linc allows quantification over lambda-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 co-induction on both first-order and higher-order encodings of perational semantics. We prove the cut-elimination and the consistency results for Linc, extending the reducibility technique due to Tait and Martin-Loef. 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 pi-calculus, where we show that the notion of names in the calculus can naturally be interpreted in the quantification theory of Linc.