Bertinoro August

English
22 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 12
Language English
Report a problem
eBtrniro,o5uAugts0250AProofTheoreticApproachtoOperationalSemantics(Focusonbinders)DaleMiller,INRIA-FutursandLIX,E´colePolytechniqueBasedontechnicalresultsin:M&Tiu:“AProofTheoryforGenericJudgments”,LICS03Tiu&M:“AProofSearchSpecificationoftheπ-Calculus”,FGUC04Tiu:“ModelCheckingforπ-CalculusUsingProofSearch”,CONCUR05Ziegler,M,Palamidessi:“Acongruenceformatforname-passingcalculi”,SOS0522/1
eBtrniro,o5uAugts0250Twoslogansaboutbindings(I)FromAlanPerlis’sEpigramsonProgramming:AsWillRogerswouldhavesaid,“Thereisnosuchthingasafreevariable.(II)Thenamesofbindersarethesamekindoffictionaswhitespace:theyareartifactsofhowwewriteexpressionsandhavezerosemanticcontent.Tospecifyorimplementalogicfordealingwithbindings,onemust,ofcourse,dealwiththecomplexityofnames.2/22Churchprovidedaspecificationofsuchalogicin1940withhispaperon“AFormulationoftheSimpleTheoryofTypes.”WeshallworkinthisParadiseof(the)Church.