Higher order quantification and proof search

Description

Niveau: Supérieur
March 2002 1 Higher-order quantification and proof search Extended abstract Dale Miller, Penn State University Sept 2002: INRIA and Ecole Polytechnique Outline 1. Security protocols, multisets rewriting, linear logic. 2. Higher-order quantifier: encrypted data as an abstract datatype. 3. Higher-order quantifier: hiding names for continuations 4. Asynchronous, synchronous, and bipolar formulas Full version of paper: AMAST 2002, 9-13 September 2002, Reunion Island.

• needham-schroeder shared


• abstract datatype


• agent memory


• bob


• support ?-conversion


• meta-theory can


• such specifications


• key protocol

Sujets

• École polytechnique
• Universidad Estatal de Pensilvania
• Abstract data type

Informations

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

Extrait

March2002 Outline Higher-orderquantificationandproofsearch Extendedabstract DaleMiller,PennStateUniversity Sept2002:INRIAandE ´ colePolytechnique 1.Securityprotocols,multisetsrewriting,linearlogic. 2.Higher-orderquantifier:encrypteddataasanabstractdatatype. 3.Higher-orderquantifier:hidingnamesforcontinuations 4.Asynchronous,synchronous,andbipolarformulas Fullversionofpaper:AMAST2002,9-13September2002,ReunionIsland. 1