Bertinoro August

Description

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

Sujets

• École polytechnique
• Rogers
• Computer programming
• No Such Thing

Informations

• Publié par: chaeh
• Nombre de lectures: 12
• Langue: English

Extrait

eBtrniro,o5uAugts0250 AProofTheoreticApproachtoOperational Semantics (Focusonbinders) DaleMiller,INRIA-FutursandLIX,E ´ colePolytechnique Basedontechnicalresultsin: •M&Tiu:“AProofTheoryforGenericJudgments”,LICS03 •Tiu&M:“AProofSearchSpecificationofthe π -Calculus”, FGUC04 •Tiu:“ModelCheckingfor π -CalculusUsingProofSearch”, CONCUR05 •Ziegler,M,Palamidessi:“Acongruenceformatforname-passing calculi”,SOS05 22/1

eBtrniro,o5uAugts0250 Twoslogansaboutbindings (I)FromAlanPerlis’sEpigramsonProgramming:AsWillRogers wouldhavesaid,“Thereisnosuchthingasafreevariable.” (II)Thenamesofbindersarethesamekindoffictionaswhite space:theyareartifactsofhowwewriteexpressionsandhavezero semanticcontent. Tospecifyorimplementalogicfordealingwithbindings,one must,ofcourse,dealwiththecomplexityofnames. 2/22 Churchprovidedaspecificationofsuchalogicin1940withhis paperon“AFormulationoftheSimpleTheoryofTypes.”Weshall workinthisParadiseof(the)Church.