DocumentCode :
1615739
Title :
A proof theory for generic judgments: an extended abstract
Author :
Miller, Dale ; Tiu, Alwen
Author_Institution :
Futurs, INRIA, France
fYear :
2003
Firstpage :
118
Lastpage :
127
Abstract :
A powerful and declarative means of specifying computations containing abstractions involves meta-level, universally quantified generic judgments. We present a proof theory for such judgments in which signatures are associated to each sequent (used to account for eigenvariables of sequent) and to each formula in the sequent (used to account for generic variables locally scoped over the formula). A new quantifier, ∇, is introduced to explicitly manipulate the local signature. Intuitionistic logic extended with ∇ satisfies cut-elimination even when the logic is additionally strengthened with a proof theoretic notion of definitions. The resulting logic can be used to encode naturally a number of examples involving name abstractions, and we illustrate using the π-calculus and the encoding of object-level provability.
Keywords :
eigenvalues and eigenfunctions; inference mechanisms; theorem proving; cut-elimination; declarative mean; extended abstract; generic judgement; generic variable; higher-order abstract syntax; intuitionistic logic; meta-level quantified generic judgment; mu-calculus; name abstraction; object-level provability; operational semantics; powerful mean; proof search; proof theory; reasoning; sequent eigenvariable; universally quantified generic judgment; Computer science; Logic;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2003. Proceedings. 18th Annual IEEE Symposium on
ISSN :
1043-6871
Print_ISBN :
0-7695-1884-2
Type :
conf
DOI :
10.1109/LICS.2003.1210051
Filename :
1210051
Link To Document :
بازگشت