A Proof Theory for Generic Judgments: An extended abstract

pages

English

Documents

Écrit par
Dale Miller

Publié par
chaeh

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

Niveau: Supérieur
A Proof Theory for Generic Judgments: An extended abstract Dale Miller INRIA/Futurs/Saclay & Ecole polytechnique Alwen Tiu Ecole polytechnique & Penn State University Abstract A powerful and declarative means of specifying com- putations containing abstractions involves meta-level, uni- versally quantified generic judgments. We present a proof theory for such judgments in which signatures are associ- ated 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 for- mula). A new quantifier, ?, is introduced to explicitly ma- nipulate the local signature. Intuitionistic logic extended with ? satisfies cut-elimination even when the logic is ad- ditionally strengthened with a proof theoretic notion of defi- nitions. 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. Keywords: proof search, reasoning about operational se- mantics, generic judgments, higher-order abstract syntax. 1. Eigenvariables and generic reasoning In specifying and reasoning about computations involv- ing abstractions, one needs to encode both the static struc- ture of such abstractions and their dynamic structure during computation.

variable can

also say

denote judgments

signature de ?

local signatures

provable using definition

scope

introduction rules

free proof

logical constants

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

A Proof Theory for Generic Judgments: An extended abstract

Dale Miller ´ INRIA/Futurs/Saclay & Ecole polytechnique dale.miller@inria.fr

Abstract

A powerful and declarative means of specifying com putations containing abstractions involves metalevel, uni versally quantiﬁedgeneric judgments. We present a proof theory for such judgments in which signatures are associ ated 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 for mula). A new quantiﬁer,r, is introduced to explicitly ma nipulate the local signature. Intuitionistic logic extended withrsatisﬁes cutelimination even when the logic is ad ditionally strengthened with a proof theoretic notion of deﬁ nitions. 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:proof search, reasoning about operational se mantics, generic judgments, higherorder abstract syntax.

1. Eigenvariables and generic reasoning

In specifying and reasoning about computations involv ing abstractions, one needs to encode both the static struc ture of such abstractions and their dynamic structure during computation. One successful approach to such an encod ing, generally calledhigherorder abstract syntax[22], uses λterms to encode the static structure of abstractions and universally quantiﬁed judgments to encode their dynamic structure. There are, of course, several ways to prove a univer sally quantiﬁed expression,∀γx.Bapproach that can. An be called theextensional, attempts to proveB[t/x]for all (closed) termstof typeγ. This rule might involve an in ﬁnite number of premises if the domain of the typeγis inﬁnite. If the typeγis deﬁned inductively, a proof byin ductioncan replace the need for inﬁnite premises with ﬁnite premises (thebasecases andinductivecases) but with the

Alwen Tiu ´ Ecole polytechnique & Penn State University tiu@cse.psu.edu

need to discover invariants. Another moreintensionalap proach, however, involves introducing a new, generic vari able, say,c:γ, that has not been introduced before in the proof, and to prove the formulaB[c/x]naturalinstead. In deduction and sequent calculus proofs, such new variables are calledeigenvariables. In Gentzen’s original presentation of the sequent cal culus [5], eigenvariables were immutable: reading proofs bottomup, once an eigenvariable is introduced it is not used as a site for substitution. In other words, Gentzen’s eigen variables did not vary in proof construction: rather they acted more as fresh, scoped constants. The generic interpretation of quantiﬁers generally entails the extensional interpretation: this is a simple consequence of the cutelimination theorem as follows. Assume that the sequent−→ ∀x.Bis proved using the introduction of∀ on the right from the premise−→B[c/x], wherecis an eigenvariable and(c)is a proof of this premise. Sim 0 ilarly, assume that the sequent,∀xB−→Cis proved using the introduction of∀on the left from the premise 0 , B[t/x]−→C, wheretis some term. To reduce the rank of the cut formula∀x.Bbetween the sequents−→ ∀x.B 0 and,∀xB−→C, the eigenvariablecin the sequent cal culus proof(c)must be substituted bytto yield a proof (t)of−→B[t/x]: in this way, the cutformula is now the smaller formulaB[t/x]Gentzen, this role of. In cin (c)as a site for substitution only takes place in the meta theory of proofs and not in proofs themselves. Recent years have witnessed two different developments in the role of eigenvariables in the speciﬁcation of compu tation systems.

Eigenvariables as fresh, scoped constantsFocusing on theirintensionalnature and guarantee of newness or fresh ness in proof search, eigenvariables have been used to en code name restrictions in theπcalculus [15], nonces in se curity protocols [1], reference locations in imperative pro gramming [2, 16], and constructors hidden within abstract datatypes [12]. Eigenvariables also provide an essential

Voir

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

A Proof Theory for Generic Judgments: An extended abstract

YouScribe

Le catalogue

Le service

Les conditions