Logic in Computer Science, Symposium on (2003)

Ottawa, Canada

June 22, 2003 to June 25, 2003

ISSN: 1043-6871

ISBN: 0-7695-1884-2

pp: 118

Dale Miller , INRIA/Futurs/Saclay & ?cole polytechnique

Alwen Tiu , ?cole polytechnique & Penn State University

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 the sequent) and to each formula in the sequent (used to account for generic variables locally scoped over the formula). A new quantifier, \bigtriangledown, is introduced to explicitly manipulate the local signature. Intuitionistic logic extended with \bigtriangledown 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 \pi-calculus and the encoding of object-level provability.

INDEX TERMS

proof search, reasoning about operational semantics, generic judgments, higher-order abstract syntax

CITATION

D. Miller and A. Tiu, "A Proof Theory for Generic Judgments: An extended abstract,"

*Logic in Computer Science, Symposium on(LICS)*, Ottawa, Canada, 2003, pp. 118.

doi:10.1109/LICS.2003.1210051

CITATIONS