CSL04 September

Description

Niveau: Supérieur
CSL04, 22 September 2004 1/27 Bindings, mobility of bindings, and the ?-quantifier Dale Miller, INRIA-Futurs and LIX, Ecole Polytechnique Based on technical results in: “A Proof Theory for Generic Judgments”, LICS2003 & ACM ToCL “A Proof Search Specification of the pi-Calculus”, Workshop on the Foundations of Global Ubiquitous Computing, 2004. Papers and work are joint with Alwen Tiu (PhD 2004; soon post doc at Loria, Nancy)

• during computation


• typed ?-expressions


• higher-order abstract


• abstract syntax


• no such thing


• typeof d?x


• logical constants

Sujets

• École polytechnique
• Rogers
• Abstract syntax
• No Such Thing
• Logical constant

Informations

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

Extrait

CSL04,22September2004 Bindings,mobilityofbindings,andthe r-quantifier DaleMiller,INRIA-FutursandLIX,E ´ colePolytechnique Basedontechnicalresultsin: 72/1 “AProofTheoryforGenericJudgments”,LICS2003&ACMToCL “AProofSearchSpecificationoftheπ-Calculus”,Workshoponthe FoundationsofGlobalUbiquitousComputing,2004. PapersandworkarejointwithAlwenTiu (PhD2004;soonpostdocatLoria,Nancy)

CSL04,22September2004 Outline 1.Abstractsyntaxforbinders 2.Genericjudgmentsandther-quantification 3.Inferencerulesfornon-logicalconstantsandequality 4.Example:π-calculus 72/2