TY - JOUR

T1 - A Logic for Reasoning about Generic Judgments

AU - Tiu, Alwen

PY - 2007/6/2

Y1 - 2007/6/2

N2 - This paper presents an extension of a proof system for encoding generic judgments, the logic FOλΔ ∇ of Miller and Tiu, with an induction principle. The logic FOλΔ ∇ is itself an extension of intuitionistic logic with fixed points and a "generic quantifier", ∇, which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλΔ ∇ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on ∇, in particular by adding the axiom B ≡ ∇ x . B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated.

AB - This paper presents an extension of a proof system for encoding generic judgments, the logic FOλΔ ∇ of Miller and Tiu, with an induction principle. The logic FOλΔ ∇ is itself an extension of intuitionistic logic with fixed points and a "generic quantifier", ∇, which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλΔ ∇ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on ∇, in particular by adding the axiom B ≡ ∇ x . B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated.

KW - Proof theory

KW - higher-order abstract syntax

KW - logical frameworks

UR - http://www.scopus.com/inward/record.url?scp=34249039887&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.01.016

DO - 10.1016/j.entcs.2007.01.016

M3 - Article

SN - 1571-0661

VL - 174

SP - 3

EP - 18

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 5

ER -