Bertinoro August

pages

English

Documents

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

Documents

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
Bertinoro, 5 August 2005 1/22 A Proof Theoretic Approach to Operational Semantics (Focus on binders) Dale Miller, INRIA-Futurs and LIX, Ecole Polytechnique Based on technical results in: • M & Tiu: “A Proof Theory for Generic Judgments”, LICS03 • Tiu & M: “A Proof Search Specification of the pi-Calculus”, FGUC04 • Tiu: “Model Checking for pi-Calculus Using Proof Search”, CONCUR05 • Ziegler, M, Palamidessi: “A congruence format for name-passing calculi”, SOS05

typed ?-expressions modulo

higher-order abstract

programming

no such thing

contain binders

function coincide

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

eBtrniro,o5uAugts0250AProofTheoreticApproachtoOperationalSemantics(Focusonbinders)DaleMiller,INRIA-FutursandLIX,E´colePolytechniqueBasedontechnicalresultsin:•M&Tiu:“AProofTheoryforGenericJudgments”,LICS03•Tiu&M:“AProofSearchSpeciﬁcationoftheπ-Calculus”,FGUC04•Tiu:“ModelCheckingforπ-CalculusUsingProofSearch”,CONCUR05•Ziegler,M,Palamidessi:“Acongruenceformatforname-passingcalculi”,SOS0522/1

eBtrniro,o5uAugts0250Twoslogansaboutbindings(I)FromAlanPerlis’sEpigramsonProgramming:AsWillRogerswouldhavesaid,“Thereisnosuchthingasafreevariable.”(II)Thenamesofbindersarethesamekindofﬁctionaswhitespace:theyareartifactsofhowwewriteexpressionsandhavezerosemanticcontent.Tospecifyorimplementalogicfordealingwithbindings,onemust,ofcourse,dealwiththecomplexityofnames.2/22Churchprovidedaspeciﬁcationofsuchalogicin1940withhispaperon“AFormulationoftheSimpleTheoryofTypes.”WeshallworkinthisParadiseof(the)Church.

Voir