publications:
- title: "Verified interoperable implementations of security protocols"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Stephen Tse"
    link: "https://researchr.org/alias/stephen-tse"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1452044.1452049"
  links:
    doi: "http://doi.acm.org/10.1145/1452044.1452049"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/BhargavanFGT08"
  cites: 0
  citedby: 0
  journal: "TOPLAS"
  volume: "31"
  number: "1"
  kind: "article"
  key: "BhargavanFGT08"
- title: "TulaFale: A Security Tool for Web Services"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Riccardo Pucella"
    link: "https://researchr.org/alias/riccardo-pucella"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3188&spage=197"
  links:
    doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3188&spage=197"
  tags:
  - "web service"
  - "security"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanFGP03"
  cites: 0
  citedby: 0
  pages: "197-222"
  booktitle: "FMCO"
  kind: "inproceedings"
  key: "BhargavanFGP03"
- title: "Verified Interoperable Implementations of Security Protocols"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Stephen Tse"
    link: "https://researchr.org/alias/stephen-tse"
  year: "2006"
  doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.32"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.32"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/BhargavanFGT06"
  cites: 0
  citedby: 0
  pages: "139-152"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "BhargavanFGT06"
- title: "Ambient Groups and Mobility Types"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Giorgio Ghelli"
    link: "https://researchr.org/alias/giorgio-ghelli"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2000"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1872/18720333.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1872/18720333.htm"
  researchr: "https://researchr.org/publication/CardelliGG00%3A1"
  cites: 0
  citedby: 0
  pages: "333-347"
  booktitle: "ifipTCS"
  kind: "inproceedings"
  key: "CardelliGG00:1"
- title: "A compositional theory for STM Haskell"
  author:
  - name: "Johannes Borgström"
    link: "https://researchr.org/alias/johannes-borgstr%C3%A3%C2%B6m"
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1596638.1596648"
  links:
    doi: "http://doi.acm.org/10.1145/1596638.1596648"
  tags:
  - "composition"
  - "Haskell"
  researchr: "https://researchr.org/publication/BorgstromBG09"
  cites: 0
  citedby: 0
  pages: "69-80"
  booktitle: "haskell"
  kind: "inproceedings"
  key: "BorgstromBG09"
- title: "A Type Discipline for Authorization Policies"
  author:
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Sergio Maffeis"
    link: "https://researchr.org/alias/sergio-maffeis"
  year: "2005"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3444&spage=141"
  links:
    doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3444&spage=141"
  researchr: "https://researchr.org/publication/FournetGM05"
  cites: 0
  citedby: 0
  pages: "141-156"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "FournetGM05"
- title: "Types for Cryptographic Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2421/24210099.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2421/24210099.htm"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/Gordon02%3A3"
  cites: 0
  citedby: 0
  pages: "99-100"
  booktitle: "concur"
  kind: "inproceedings"
  key: "Gordon02:3"
- title: "Stack inspection: theory and variants"
  author:
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  doi: "http://doi.acm.org/10.1145/503272.503301"
  links:
    doi: "http://doi.acm.org/10.1145/503272.503301"
  researchr: "https://researchr.org/publication/FournetG02"
  cites: 0
  citedby: 0
  pages: "307-318"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "FournetG02"
- title: "Preface"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  year: "1999"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#001"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#001"
  researchr: "https://researchr.org/publication/GordonP99"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "26"
  pages: "1-2"
  kind: "article"
  key: "GordonP99"
- title: "Types and effects for asymmetric cryptographic protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2004"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/GordonJ04"
  cites: 0
  citedby: 0
  journal: "jcs"
  volume: "12"
  number: "3-4"
  pages: "435-483"
  kind: "article"
  key: "GordonJ04"
- title: "Design and Semantics of a Decentralized Authorization Language"
  author:
  - name: "Moritz Y. Becker"
    link: "https://researchr.org/alias/moritz-y.-becker"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2007"
  doi: "http://dx.doi.org/10.1109/CSF.2007.18"
  links:
    doi: "http://dx.doi.org/10.1109/CSF.2007.18"
  tags:
  - "semantics"
  - "language design"
  - "design"
  researchr: "https://researchr.org/publication/BeckerFG07"
  cites: 0
  citedby: 0
  pages: "3-15"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "BeckerFG07"
- title: "From Stack Inspection to Access Control: A Security Analysis for Libraries"
  author:
  - name: "Frédéric Besson"
    link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-besson"
  - name: "Tomasz Blanc"
    link: "https://researchr.org/alias/tomasz-blanc"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2004"
  doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.11"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.11"
  tags:
  - "analysis"
  - "security"
  - "access control"
  researchr: "https://researchr.org/publication/BessonBFG04"
  cites: 0
  citedby: 0
  pages: "61"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "BessonBFG04"
- title: "A Hybrid Expert System for IT Security Risk Assessment"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Ivan Belik"
    link: "https://researchr.org/alias/ivan-belik"
  - name: "Shahram Rahimi"
    link: "https://researchr.org/alias/shahram-rahimi"
  year: "2010"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pdpta/GordonBR10"
  tags:
  - "security"
  researchr: "https://researchr.org/publication/GordonBR10"
  cites: 0
  citedby: 0
  pages: "430-434"
  booktitle: "pdpta"
  kind: "inproceedings"
  key: "GordonBR10"
- title: "Compilation and Equivalence of Imperative Objects"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Paul D. Hankin"
    link: "https://researchr.org/alias/paul-d.-hankin"
  - name: "Søren B. Lassen"
    link: "https://researchr.org/alias/s%C3%B8ren-b.-lassen"
  year: "1999"
  tags:
  - "meta-model"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/GordonHL99"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "9"
  number: "4"
  pages: "373-426"
  kind: "article"
  key: "GordonHL99"
- title: "SecPAL: Design and semantics of a decentralized authorization language"
  author:
  - name: "Moritz Y. Becker"
    link: "https://researchr.org/alias/moritz-y.-becker"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2010"
  doi: "http://dx.doi.org/10.3233/JCS-2009-0364"
  abstract: "We present a declarative authorization language. Policies and credentials are expressed using predicates defined by logical clauses, in the style of constraint logic programming. Access requests are mapped to logical authorization queries, consisting of predicates and constraints combined by conjunctions, disjunctions, and negations. Access is granted if the query succeeds against the current database of clauses. Predicates ascribe rights to particular principals, with flexible support for delegation and revocation. At the discretion of the delegator, delegated rights can be further delegated, either to a fixed depth, or arbitrarily deeply. Our language strikes a careful balance between syntactic and semantic simplicity, policy expressiveness, and execution efficiency. The syntax is close to natural language, and the semantics consists of just three deduction rules. The language can express many common policy idioms using constraints, controlled delegation, recursive predicates, and negated queries. We describe an execution strategy based on translation to Datalog with Constraints, and table-based resolution. We show that this execution strategy is sound, complete, and always terminates, despite recursion and negation, as long as simple syntactic conditions are met."
  links:
    doi: "http://dx.doi.org/10.3233/JCS-2009-0364"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jcs/BeckerFG10"
  tags:
  - "programming languages"
  - "semantics"
  - "rule-based"
  - "translation"
  - "completeness"
  - "language design"
  - "constraints"
  - "rules"
  - "logic programming"
  - "programming"
  - "database"
  - "logic"
  - "access control policies"
  - "access control"
  - "Datalog"
  - "design"
  - "role-based access control"
  - "query language"
  researchr: "https://researchr.org/publication/BeckerFG10"
  cites: 0
  citedby: 0
  journal: "jcs"
  volume: "18"
  number: "4"
  pages: "619-665"
  kind: "article"
  key: "BeckerFG10"
- title: "A Type and Effect Analysis of Security Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2001"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2126/21260432.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2126/21260432.htm"
  tags:
  - "protocol"
  - "analysis"
  - "security"
  researchr: "https://researchr.org/publication/GordonJ01%3A1"
  cites: 0
  citedby: 0
  pages: "432"
  booktitle: "SAS"
  kind: "inproceedings"
  key: "GordonJ01:1"
- title: "Branching Storylines in Virtual Reality Environments for Leadership Development"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Michael van Lent"
    link: "https://researchr.org/alias/michael-van-lent"
  - name: "Martin Van Velsen"
    link: "https://researchr.org/alias/martin-van-velsen"
  - name: "Paul Carpenter"
    link: "https://researchr.org/alias/paul-carpenter"
  - name: "Arnav Jhala"
    link: "https://researchr.org/alias/arnav-jhala"
  year: "2004"
  tags:
  - "Meta-Environment"
  researchr: "https://researchr.org/publication/GordonLVCJ04"
  cites: 0
  citedby: 0
  pages: "844-851"
  booktitle: "AAAI"
  kind: "inproceedings"
  key: "GordonLVCJ04"
- title: "Type Inference for Correspondence Types"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Hans Hüttel"
    link: "https://researchr.org/alias/hans-h%C3%A3%C2%BCttel"
  - name: "René Rydhof Hansen"
    link: "https://researchr.org/alias/ren%C3%A3%C2%A9-rydhof-hansen"
  year: "2009"
  doi: "http://dx.doi.org/10.1016/j.entcs.2009.07.079"
  abstract: "We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E, generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable. "
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2009.07.079"
  tags:
  - "type inference"
  - "meta-model"
  - "modeling"
  - "constraints"
  - "type system"
  - "e-science"
  - "logic"
  - "Meta-Environment"
  - "process modeling"
  researchr: "https://researchr.org/publication/GordonHH09"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "242"
  number: "3"
  pages: "21-36"
  kind: "article"
  key: "GordonHH09"
- title: "Preface"
  author:
  - name: "Luca Aceto"
    link: "https://researchr.org/alias/luca-aceto"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2006"
  doi: "http://dx.doi.org/10.1016/j.entcs.2005.12.100"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2005.12.100"
  researchr: "https://researchr.org/publication/AcetoG06"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "162"
  pages: "1-2"
  kind: "article"
  key: "AcetoG06"
- title: "Reasoning about Cryptographic Protocols in the Spi Calculus"
  author:
  - name: "Martín Abadi"
    link: "http://users.soe.ucsc.edu/~abadi/home.html"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1997"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/AbadiG97%3A0"
  cites: 0
  citedby: 0
  pages: "59-73"
  booktitle: "concur"
  kind: "inproceedings"
  key: "AbadiG97:0"
- title: "Refinement Types for Secure Implementations"
  author:
  - name: "Jesper Bengtson"
    link: "https://researchr.org/alias/jesper-bengtson"
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Sergio Maffeis"
    link: "https://researchr.org/alias/sergio-maffeis"
  year: "2008"
  doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27"
  tags:
  - "refinement"
  researchr: "https://researchr.org/publication/BengtsonBFGM08"
  cites: 0
  citedby: 0
  pages: "17-32"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "BengtsonBFGM08"
- title: "Bisimilarity as a Theory of Functional Programming"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1999"
  doi: "http://dx.doi.org/10.1016/S0304-3975(98)00353-3"
  links:
    doi: "http://dx.doi.org/10.1016/S0304-3975(98)00353-3"
  tags:
  - "functional programming"
  - "programming"
  researchr: "https://researchr.org/publication/Gordon99"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "228"
  number: "1-2"
  pages: "5-47"
  kind: "article"
  key: "Gordon99"
- title: "A Chart Semantics for the Pi-Calculus"
  author:
  - name: "Johannes Borgström"
    link: "https://researchr.org/alias/johannes-borgstr%C3%B6m"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Andrew Phillips"
    link: "https://researchr.org/alias/andrew-phillips"
  year: "2008"
  doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.002"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.002"
  tags:
  - "semantics"
  researchr: "https://researchr.org/publication/BorgstromGP08"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "194"
  number: "2"
  pages: "3-29"
  kind: "article"
  key: "BorgstromGP08"
- title: "Verified implementations of the information card federated identity-management protocol"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Nikhil Swamy"
    link: "https://researchr.org/alias/nikhil-swamy"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1368310.1368330"
  links:
    doi: "http://doi.acm.org/10.1145/1368310.1368330"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/BhargavanFGS08"
  cites: 0
  citedby: 0
  pages: "123-135"
  booktitle: "ccs"
  kind: "inproceedings"
  key: "BhargavanFGS08"
- title: "Validating a Web service security abstraction by typing"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Riccardo Pucella"
    link: "https://researchr.org/alias/riccardo-pucella"
  year: "2002"
  doi: "http://doi.acm.org/10.1145/764792.764797"
  links:
    doi: "http://doi.acm.org/10.1145/764792.764797"
  tags:
  - "web service"
  - "security"
  - "abstraction"
  researchr: "https://researchr.org/publication/GordonP02"
  cites: 0
  citedby: 0
  pages: "18-29"
  booktitle: "xmlsec"
  kind: "inproceedings"
  key: "GordonP02"
- title: "Authenticity Types for Cryptographic Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2629&spage=3"
  links:
    doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2629&spage=3"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/Gordon02%3A1"
  cites: 0
  citedby: 0
  pages: "3"
  booktitle: "fasec"
  kind: "inproceedings"
  key: "Gordon02:1"
- title: "A Bisimulation Method for Cryptographic Protocols"
  author:
  - name: "Martín Abadi"
    link: "https://researchr.org/alias/mart%C3%ADn-abadi"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1998"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/AbadiG98%3A0"
  cites: 0
  citedby: 0
  journal: "njc"
  volume: "5"
  number: "4"
  pages: "267"
  kind: "article"
  key: "AbadiG98:0"
- title: "Finite-Control Mobile Ambients"
  author:
  - name: "Witold Charatonik"
    link: "https://researchr.org/alias/witold-charatonik"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Jean-Marc Talbot"
    link: "https://researchr.org/alias/jean-marc-talbot"
  year: "2002"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2305/23050295.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2305/23050295.htm"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/CharatonikGT02"
  cites: 0
  citedby: 0
  pages: "295-313"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "CharatonikGT02"
- title: "Service Combinators for Farming Virtual Machines"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Iman Narasamdya"
    link: "https://researchr.org/alias/iman-narasamdya"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_3"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_3"
  researchr: "https://researchr.org/publication/BhargavanGN07"
  cites: 0
  citedby: 0
  pages: "22"
  booktitle: "tgc"
  kind: "inproceedings"
  key: "BhargavanGN07"
- title: "An Operational Semantics for I/O in a Lazy Functional Language"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1993"
  tags:
  - "laziness"
  - "semantics"
  - "operational semantics"
  researchr: "https://researchr.org/publication/Gordon93%3A2"
  cites: 0
  citedby: 0
  pages: "136-145"
  booktitle: "fpca"
  kind: "inproceedings"
  key: "Gordon93:2"
- title: "Modular verification of security protocol code by typing"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A3%C2%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1706299.1706350"
  links:
    doi: "http://doi.acm.org/10.1145/1706299.1706350"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/BhargavanFG10"
  cites: 0
  citedby: 0
  pages: "445-456"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "BhargavanFG10"
- title: "Model checking mobile ambients"
  author:
  - name: "Witold Charatonik"
    link: "https://researchr.org/alias/witold-charatonik"
  - name: "Silvano Dal-Zilio"
    link: "https://researchr.org/alias/silvano-dal-zilio"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Supratik Mukhopadhyay"
    link: "https://researchr.org/alias/supratik-mukhopadhyay"
  - name: "Jean-Marc Talbot"
    link: "https://researchr.org/alias/jean-marc-talbot"
  year: "2003"
  doi: "http://dx.doi.org/10.1016/S0304-3975(02)00832-0"
  links:
    doi: "http://dx.doi.org/10.1016/S0304-3975(02)00832-0"
  tags:
  - "model checking"
  - "meta-model"
  - "Meta-Environment"
  - "mobile"
  researchr: "https://researchr.org/publication/CharatonikDGMT03"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "308"
  number: "1-3"
  pages: "277-331"
  kind: "article"
  key: "CharatonikDGMT03"
- title: "A semantics for web services authentication"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2005"
  doi: "http://dx.doi.org/10.1016/j.tcs.2005.03.005"
  links:
    doi: "http://dx.doi.org/10.1016/j.tcs.2005.03.005"
  tags:
  - "semantics"
  - "web service"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanFG05"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "340"
  number: "1"
  pages: "102-153"
  kind: "article"
  key: "BhargavanFG05"
- title: "Verifying policy-based security for web services"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/1030083.1030120"
  links:
    doi: "http://doi.acm.org/10.1145/1030083.1030120"
  tags:
  - "rule-based"
  - "web service"
  - "security"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanFG04"
  cites: 0
  citedby: 0
  pages: "268-277"
  booktitle: "ccs"
  kind: "inproceedings"
  key: "BhargavanFG04"
- title: "Preface"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  - name: "Carolyn L. Talcott"
    link: "https://researchr.org/alias/carolyn-l.-talcott"
  year: "1997"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#001"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#001"
  researchr: "https://researchr.org/publication/GordonPT97"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "10"
  pages: "1"
  kind: "article"
  key: "GordonPT97"
- title: "Types for Cyphers: Thwarting Mischief and Malice with Type Theory"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2001"
  tags:
  - "type theory"
  researchr: "https://researchr.org/publication/Gordon01"
  cites: 0
  citedby: 0
  pages: "136"
  booktitle: "ppdp"
  kind: "inproceedings"
  key: "Gordon01"
- title: "Typing correspondence assertions for communication protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2003"
  doi: "http://dx.doi.org/10.1016/S0304-3975(02)00333-X"
  links:
    doi: "http://dx.doi.org/10.1016/S0304-3975(02)00333-X"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/GordonJ03"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "300"
  number: "1-3"
  pages: "379-409"
  kind: "article"
  key: "GordonJ03"
- title: "V for Virtual"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2006"
  doi: "http://dx.doi.org/10.1016/j.entcs.2006.01.030"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2006.01.030"
  researchr: "https://researchr.org/publication/Gordon06"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "162"
  pages: "177-181"
  kind: "article"
  key: "Gordon06"
- title: "Types and Effects for Asymmetric Cryptographic Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2002"
  doi: "http://csdl.computer.org/comp/proceedings/csfw/2002/1689/00/16890077abs.htm"
  links:
    doi: "http://csdl.computer.org/comp/proceedings/csfw/2002/1689/00/16890077abs.htm"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/GordonJ02"
  cites: 0
  citedby: 0
  pages: "77-91"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "GordonJ02"
- title: "Preface for the Special Issue: Foundations of Software Science and Computation Structures"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2005"
  doi: "http://dx.doi.org/10.1016/j.tcs.2004.11.001"
  links:
    doi: "http://dx.doi.org/10.1016/j.tcs.2004.11.001"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/Gordon05%3A0"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "333"
  number: "1-2"
  pages: "1"
  kind: "article"
  key: "Gordon05:0"
- title: "Validating a web service security abstraction by typing"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Riccardo Pucella"
    link: "https://researchr.org/alias/riccardo-pucella"
  year: "2005"
  doi: "http://dx.doi.org/10.1007/s00165-004-0058-1"
  links:
    doi: "http://dx.doi.org/10.1007/s00165-004-0058-1"
  tags:
  - "web service"
  - "security"
  - "abstraction"
  researchr: "https://researchr.org/publication/GordonP05%3A0"
  cites: 0
  citedby: 0
  journal: "fac"
  volume: "17"
  number: "3"
  pages: "277-318"
  kind: "article"
  key: "GordonP05:0"
- title: "The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1992"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/Gordon92a"
  cites: 0
  citedby: 0
  pages: "531-534"
  booktitle: "iccd"
  kind: "inproceedings"
  key: "Gordon92a"
- title: "Mobility Types for Mobile Ambients"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Giorgio Ghelli"
    link: "https://researchr.org/alias/giorgio-ghelli"
  year: "1999"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1644/16440230.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1644/16440230.htm"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/CardelliGG99"
  cites: 0
  citedby: 0
  pages: "230-239"
  booktitle: "icalp"
  kind: "inproceedings"
  key: "CardelliGG99"
- title: "Logical Properties of Name Restriction"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2001"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2044/20440046.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2044/20440046.htm"
  researchr: "https://researchr.org/publication/CardelliG01%3A0"
  cites: 0
  citedby: 0
  pages: "46-60"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "CardelliG01:0"
- title: "Provable Implementations of Security Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2006"
  doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2006.43"
  links:
    doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2006.43"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/Gordon06%3A2"
  cites: 0
  citedby: 0
  pages: "345-346"
  booktitle: "lics"
  kind: "inproceedings"
  key: "Gordon06:2"
- title: "Typing Correspondence Assertions for Communication Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2001"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/88/27/show/Products/notes/index.htt#009"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/88/27/show/Products/notes/index.htt#009"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/GordonJ01"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "45"
  pages: "119-140"
  kind: "article"
  key: "GordonJ01"
- title: "Guest Editors  Foreword"
  author:
  - name: "Luca Aceto"
    link: "https://researchr.org/alias/luca-aceto"
  - name: "Mario Bravetti"
    link: "https://researchr.org/alias/mario-bravetti"
  - name: "Wan Fokkink"
    link: "http://www.cs.vu.nl/~wanf/"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.jlap.2006.08.002"
  links:
    doi: "http://dx.doi.org/10.1016/j.jlap.2006.08.002"
  researchr: "https://researchr.org/publication/AcetoBFG07"
  cites: 0
  citedby: 0
  journal: "jlp"
  volume: "70"
  number: "2"
  pages: "119-120"
  kind: "article"
  key: "AcetoBFG07"
- title: "Mobile Ambients"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1998"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1378/13780140.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1378/13780140.htm"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/CardelliG98"
  cites: 0
  citedby: 0
  pages: "140-155"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "CardelliG98"
- title: "Authenticity by Typing for Security Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2003"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/GordonJ03%3A0"
  cites: 0
  citedby: 0
  journal: "jcs"
  volume: "11"
  number: "4"
  pages: "451-520"
  kind: "article"
  key: "GordonJ03:0"
- title: "Deciding validity in a spatial logic for trees"
  author:
  - name: "Cristiano Calcagno"
    link: "https://researchr.org/alias/cristiano-calcagno"
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/604174.604183"
  links:
    doi: "http://doi.acm.org/10.1145/604174.604183"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/CalcagnoCG03"
  cites: 0
  citedby: 0
  pages: "62-73"
  booktitle: "tldi"
  kind: "inproceedings"
  key: "CalcagnoCG03"
- title: "A Sound Metalogical Semantics for Input/Output Effects"
  author:
  - name: "Roy L. Crole"
    link: "https://researchr.org/alias/roy-l.-crole"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1994"
  tags:
  - "semantics"
  researchr: "https://researchr.org/publication/CroleG94"
  cites: 0
  citedby: 0
  pages: "339-353"
  booktitle: "csl"
  kind: "inproceedings"
  key: "CroleG94"
- title: "XML Web Services: The Global Computer?"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  tags:
  - "XML"
  - "XML Schema"
  - "web service"
  - "web services"
  researchr: "https://researchr.org/publication/Gordon02%3A0"
  cites: 0
  citedby: 0
  pages: "355"
  booktitle: "ifipTCS"
  kind: "inproceedings"
  key: "Gordon02:0"
- title: "A semantics for web services authentication"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/964001.964018"
  abstract: "We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Security describes a range of XML security tokens, such as username tokens, public-key certificates, and digital signature blocks, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these tokens, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security tokens and of sample protocols distributed with the Microsoft WSE implementation of WS-Security. By embedding our data model within Abadi and Fournet's applied pi calculus, we formulate and prove security properties with respect to the standard Dolev-Yao threat model. Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format. "
  links:
    doi: "http://doi.acm.org/10.1145/964001.964018"
  tags:
  - "semantics"
  - "rule-based"
  - "formal semantics"
  - "meta-model"
  - "XML"
  - "XML Schema"
  - "protocol"
  - "web service"
  - "data-flow"
  - "certification"
  - "security"
  - "web services"
  - "Meta-Environment"
  - "systematic-approach"
  researchr: "https://researchr.org/publication/BhargavanFG04%3A0"
  cites: 0
  citedby: 0
  pages: "198-209"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "BhargavanFG04:0"
- title: "Secrecy, Group Creation"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Giorgio Ghelli"
    link: "https://researchr.org/alias/giorgio-ghelli"
  year: "2000"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/97/27/show/Products/notes/index.htt#006"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/97/27/show/Products/notes/index.htt#006"
  researchr: "https://researchr.org/publication/CardelliGG00"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "40"
  pages: "7"
  kind: "article"
  key: "CardelliGG00"
- title: "Five Axioms of Alpha-Conversion"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Thomas F. Melham"
    link: "https://researchr.org/alias/thomas-f.-melham"
  year: "1996"
  researchr: "https://researchr.org/publication/GordonM96"
  cites: 0
  citedby: 0
  pages: "173-190"
  booktitle: "tphol"
  kind: "inproceedings"
  key: "GordonM96"
- title: "Recognizing Expressions of Commonsense Psychology in English Text"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Abe Kazemzadeh"
    link: "https://researchr.org/alias/abe-kazemzadeh"
  - name: "Anish Nair"
    link: "https://researchr.org/alias/anish-nair"
  - name: "Milena Petrova"
    link: "https://researchr.org/alias/milena-petrova"
  year: "2003"
  doi: "http://acl.ldc.upenn.edu/acl2003/main/pdfs/Gordon.pdf"
  links:
    doi: "http://acl.ldc.upenn.edu/acl2003/main/pdfs/Gordon.pdf"
  researchr: "https://researchr.org/publication/GordonKNP03"
  cites: 0
  citedby: 0
  pages: "208-215"
  booktitle: "acl"
  kind: "inproceedings"
  key: "GordonKNP03"
- title: "The Complexity of Model Checking Mobile Ambients"
  author:
  - name: "Witold Charatonik"
    link: "https://researchr.org/alias/witold-charatonik"
  - name: "Silvano Dal-Zilio"
    link: "https://researchr.org/alias/silvano-dal-zilio"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Supratik Mukhopadhyay"
    link: "https://researchr.org/alias/supratik-mukhopadhyay"
  - name: "Jean-Marc Talbot"
    link: "https://researchr.org/alias/jean-marc-talbot"
  year: "2001"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2030/20300152.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2030/20300152.htm"
  tags:
  - "model checking"
  - "meta-model"
  - "Meta-Environment"
  - "mobile"
  researchr: "https://researchr.org/publication/CharatonikDGMT01"
  cites: 0
  citedby: 0
  pages: "152-167"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "CharatonikDGMT01"
- title: "Types for the Ambient Calculus"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Giorgio Ghelli"
    link: "https://researchr.org/alias/giorgio-ghelli"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  doi: "http://dx.doi.org/10.1006/inco.2001.3121"
  links:
    doi: "http://dx.doi.org/10.1006/inco.2001.3121"
  researchr: "https://researchr.org/publication/CardelliGG02"
  cites: 0
  citedby: 0
  journal: "iandc"
  volume: "177"
  number: "2"
  pages: "160-194"
  kind: "article"
  key: "CardelliGG02"
- title: "Secrecy and Group Creation"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Giorgio Ghelli"
    link: "https://researchr.org/alias/giorgio-ghelli"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2000"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1877/18770365.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1877/18770365.htm"
  researchr: "https://researchr.org/publication/CardelliGG00%3A0"
  cites: 0
  citedby: 0
  pages: "365-379"
  booktitle: "concur"
  kind: "inproceedings"
  key: "CardelliGG00:0"
- title: "Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2005"
  doi: "http://dx.doi.org/10.1007/11539452_17"
  links:
    doi: "http://dx.doi.org/10.1007/11539452_17"
  researchr: "https://researchr.org/publication/GordonJ05"
  cites: 0
  citedby: 0
  pages: "186-201"
  booktitle: "concur"
  kind: "inproceedings"
  key: "GordonJ05"
- title: "Verified Reference Implementations of WS-Security Protocols"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/11841197_6"
  links:
    doi: "http://dx.doi.org/10.1007/11841197_6"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/BhargavanFG06"
  cites: 0
  citedby: 0
  pages: "88-106"
  booktitle: "wsfm"
  kind: "inproceedings"
  key: "BhargavanFG06"
- title: "Equational Properties Of Mobile Ambients"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  year: "2003"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/GordonC03"
  cites: 0
  citedby: 0
  journal: "mscs"
  volume: "13"
  number: "3"
  pages: "371-408"
  kind: "article"
  key: "GordonC03"
- title: "Anytime, Anywhere: Modal Logics for Mobile Ambients"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/325694.325742"
  links:
    doi: "http://doi.acm.org/10.1145/325694.325742"
  tags:
  - "modal logic"
  - "logic"
  - "mobile"
  researchr: "https://researchr.org/publication/CardelliG00"
  cites: 0
  citedby: 0
  pages: "365-377"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "CardelliG00"
- title: "Region Analysis and a pi-Calculus wiht Groups"
  author:
  - name: "Silvano Dal-Zilio"
    link: "https://researchr.org/alias/silvano-dal-zilio"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2000"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1893/18930001.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1893/18930001.htm"
  tags:
  - "analysis"
  researchr: "https://researchr.org/publication/Dal-ZilioG00"
  cites: 0
  citedby: 0
  pages: "1-20"
  booktitle: "mfcs"
  kind: "inproceedings"
  key: "Dal-ZilioG00"
- title: "A type discipline for authorization policies"
  author:
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Sergio Maffeis"
    link: "https://researchr.org/alias/sergio-maffeis"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1275497.1275500"
  links:
    doi: "http://doi.acm.org/10.1145/1275497.1275500"
  researchr: "https://researchr.org/publication/FournetGM07"
  cites: 0
  citedby: 0
  journal: "TOPLAS"
  volume: "29"
  number: "5"
  pages: "25"
  kind: "article"
  key: "FournetGM07"
- title: "A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1993"
  researchr: "https://researchr.org/publication/Gordon93%3A0"
  cites: 0
  citedby: 0
  pages: "413-425"
  booktitle: "tphol"
  kind: "inproceedings"
  key: "Gordon93:0"
- title: "Typing One-to-One and One-to-Many Correspondences in Security Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2002"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2609&spage=263"
  links:
    doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2609&spage=263"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/GordonJ02%3A0"
  cites: 0
  citedby: 0
  pages: "263-282"
  booktitle: "isss2"
  kind: "inproceedings"
  key: "GordonJ02:0"
- title: "Secure sessions for Web services"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Ricardo Corin"
    link: "https://researchr.org/alias/ricardo-corin"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1237500.1237504"
  links:
    doi: "http://doi.acm.org/10.1145/1237500.1237504"
  tags:
  - "web service"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanCFG07"
  cites: 0
  citedby: 0
  journal: "tissec"
  volume: "10"
  number: "2"
  pages: "8"
  kind: "article"
  key: "BhargavanCFG07"
- title: "Guided Conversations about Leadership: Mentoring with Movies and Interactive Characters"
  author:
  - name: "Randall W. Hill Jr."
    link: "https://researchr.org/alias/randall-w.-hill-jr."
  - name: "Jay Douglas"
    link: "https://researchr.org/alias/jay-douglas"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Frederic H. Pighin"
    link: "https://researchr.org/alias/frederic-h.-pighin"
  - name: "Martin Van Velsen"
    link: "https://researchr.org/alias/martin-van-velsen"
  year: "2003"
  researchr: "https://researchr.org/publication/HillDGPV03"
  cites: 0
  citedby: 0
  pages: "101-108"
  booktitle: "AAAI"
  kind: "inproceedings"
  key: "HillDGPV03"
- title: "Experience with Embedding Hardware Description Languages in HOL"
  author:
  - name: "Richard J. Boulton"
    link: "https://researchr.org/alias/richard-j.-boulton"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Michael J. C. Gordon"
    link: "https://researchr.org/alias/michael-j.-c.-gordon"
  - name: "John Harrison"
    link: "https://researchr.org/alias/john-harrison"
  - name: "John Herbert"
    link: "https://researchr.org/alias/john-herbert"
  - name: "John Van Tassel"
    link: "https://researchr.org/alias/john-van-tassel"
  year: "1992"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/BoultonGGHHT92"
  cites: 0
  citedby: 0
  pages: "129-156"
  booktitle: "tpcd"
  kind: "inproceedings"
  key: "BoultonGGHHT92"
- title: "Types for Mobile Ambients"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/292540.292550"
  links:
    doi: "http://doi.acm.org/10.1145/292540.292550"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/CardelliG99"
  cites: 0
  citedby: 0
  pages: "79-92"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "CardelliG99"
- title: "Compilation and Equivalence of Imperative Objects"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Paul D. Hankin"
    link: "https://researchr.org/alias/paul-d.-hankin"
  - name: "Søren B. Lassen"
    link: "https://researchr.org/alias/s%C3%B8ren-b.-lassen"
  year: "1997"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1346/13460074.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1346/13460074.htm"
  tags:
  - "meta-model"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/GordonHL97"
  cites: 0
  citedby: 0
  pages: "74-87"
  booktitle: "fsttcs"
  kind: "inproceedings"
  key: "GordonHL97"
- title: "Region analysis and a pi-calculus with groups"
  author:
  - name: "Silvano Dal-Zilio"
    link: "https://researchr.org/alias/silvano-dal-zilio"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  tags:
  - "analysis"
  researchr: "https://researchr.org/publication/Dal-ZilioG02"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "12"
  number: "3"
  pages: "229-292"
  kind: "article"
  key: "Dal-ZilioG02"
- title: "A Type Discipline for Authorization in Distributed Systems"
  author:
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Sergio Maffeis"
    link: "https://researchr.org/alias/sergio-maffeis"
  year: "2007"
  doi: "http://dx.doi.org/10.1109/CSF.2007.7"
  links:
    doi: "http://dx.doi.org/10.1109/CSF.2007.7"
  tags:
  - "type system"
  researchr: "https://researchr.org/publication/FournetGM07%3A0"
  cites: 0
  citedby: 0
  pages: "31-48"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "FournetGM07:0"
- title: "Code-Carrying Authorization"
  author:
  - name: "Sergio Maffeis"
    link: "https://researchr.org/alias/sergio-maffeis"
  - name: "Martín Abadi"
    link: "https://researchr.org/alias/mart%C3%ADn-abadi"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-540-88313-5_36"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-88313-5_36"
  researchr: "https://researchr.org/publication/MaffeisAFG08"
  cites: 0
  citedby: 0
  pages: "563-579"
  booktitle: "esorics"
  kind: "inproceedings"
  key: "MaffeisAFG08"
- title: "Secure sessions for web services"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Ricardo Corin"
    link: "https://researchr.org/alias/ricardo-corin"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/1111348.1111355"
  links:
    doi: "http://doi.acm.org/10.1145/1111348.1111355"
  tags:
  - "web service"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanCFG04"
  cites: 0
  citedby: 0
  pages: "56-66"
  booktitle: "sws"
  kind: "inproceedings"
  key: "BhargavanCFG04"
- title: "From Typed Process Calculi to Source-Based Security"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2005"
  doi: "http://dx.doi.org/10.1007/11547662_2"
  links:
    doi: "http://dx.doi.org/10.1007/11547662_2"
  tags:
  - "rule-based"
  - "source-to-source"
  - "security"
  - "open-source"
  researchr: "https://researchr.org/publication/Gordon05%3A1"
  cites: 0
  citedby: 0
  pages: "2"
  booktitle: "SAS"
  kind: "inproceedings"
  key: "Gordon05:1"
- title: "A Calculus for Cryptographic Protocols: The Spi Calculus"
  author:
  - name: "Martín Abadi"
    link: "https://researchr.org/alias/mart%C3%ADn-abadi"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1997"
  doi: "http://doi.acm.org/10.1145/266420.266432"
  links:
    doi: "http://doi.acm.org/10.1145/266420.266432"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/AbadiG97"
  cites: 0
  citedby: 0
  pages: "36-47"
  booktitle: "ccs"
  kind: "inproceedings"
  key: "AbadiG97"
- title: "Guest Editors  Foreword"
  author:
  - name: "Luca Aceto"
    link: "https://researchr.org/alias/luca-aceto"
  - name: "Mario Bravetti"
    link: "https://researchr.org/alias/mario-bravetti"
  - name: "Wan Fokkink"
    link: "http://www.cs.vu.nl/~wanf/"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.jlap.2007.02.001"
  links:
    doi: "http://dx.doi.org/10.1016/j.jlap.2007.02.001"
  researchr: "https://researchr.org/publication/AcetoBFG07a"
  cites: 0
  citedby: 0
  journal: "jlp"
  volume: "72"
  number: "1"
  pages: "1-2"
  kind: "article"
  key: "AcetoBFG07a"
- title: "A Concurrent Object Calculus: Reduction and Typing"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Paul D. Hankin"
    link: "https://researchr.org/alias/paul-d.-hankin"
  year: "1998"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/40/26/show/Products/notes/index.htt#007"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/40/26/show/Products/notes/index.htt#007"
  tags:
  - "meta-model"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/GordonH98"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "16"
  number: "3"
  pages: "248-264"
  kind: "article"
  key: "GordonH98"
- title: "Concurrent Haskell"
  author:
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Sigbjorn Finne"
    link: "https://researchr.org/alias/sigbjorn-finne"
  year: "1996"
  doi: "http://doi.acm.org/10.1145/237721.237794"
  links:
    doi: "http://doi.acm.org/10.1145/237721.237794"
  tags:
  - "Haskell"
  researchr: "https://researchr.org/publication/JonesGF96"
  cites: 0
  citedby: 0
  pages: "295-308"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "JonesGF96"
- title: "Mobile Ambients"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1997"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#017"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#017"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/CardelliG97"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "10"
  pages: "198-201"
  kind: "article"
  key: "CardelliG97"
- title: "Notes on Nominal Calculi for Security and Mobility"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2000"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2171/21710262.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2171/21710262.htm"
  tags:
  - "security"
  researchr: "https://researchr.org/publication/Gordon00%3A4"
  cites: 0
  citedby: 0
  pages: "262-330"
  booktitle: "fosad"
  kind: "inproceedings"
  key: "Gordon00:4"
- title: "Relating operational and denotational semantics for input/output effects"
  author:
  - name: "Roy L. Crole"
    link: "https://researchr.org/alias/roy-l.-crole"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1999"
  tags:
  - "semantics"
  - "denotational semantics"
  - "operational semantics"
  researchr: "https://researchr.org/publication/CroleG99"
  cites: 0
  citedby: 0
  journal: "mscs"
  volume: "9"
  number: "2"
  pages: "125-158"
  kind: "article"
  key: "CroleG99"
- title: "Deciding validity in a spatial logic for trees"
  author:
  - name: "Cristiano Calcagno"
    link: "https://researchr.org/alias/cristiano-calcagno"
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2005"
  doi: "http://dx.doi.org/10.1017/S0956796804005404"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796804005404"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/CalcagnoCG05"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "15"
  number: "4"
  pages: "543-572"
  kind: "article"
  key: "CalcagnoCG05"
- title: "Typing a multi-language intermediate code"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Don Syme"
    link: "https://researchr.org/alias/don-syme"
  year: "2001"
  doi: "http://doi.acm.org/10.1145/360204.360228"
  links:
    doi: "http://doi.acm.org/10.1145/360204.360228"
  researchr: "https://researchr.org/publication/GordonS01"
  cites: 0
  citedby: 0
  pages: "248-260"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "GordonS01"
- title: "Verifying policy-based web services security"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1391956.1391957"
  links:
    doi: "http://doi.acm.org/10.1145/1391956.1391957"
  tags:
  - "rule-based"
  - "web service"
  - "security"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanFG08"
  cites: 0
  citedby: 0
  journal: "TOPLAS"
  volume: "30"
  number: "6"
  kind: "article"
  key: "BhargavanFG08"
- title: "Equational Properties of Mobile Ambients"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  year: "1999"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/GordonC99"
  cites: 0
  citedby: 0
  pages: "212-226"
  booktitle: "fossacs"
  kind: "inproceedings"
  key: "GordonC99"
- title: "Bisimilarity as a theory of functional programming"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1995"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#014"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#014"
  tags:
  - "functional programming"
  - "programming"
  researchr: "https://researchr.org/publication/Gordon95%3A0"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "1"
  pages: "232-252"
  kind: "article"
  key: "Gordon95:0"
- title: "Automating Type Soundness Proofs via Decision Procedures and Guided Reductions"
  author:
  - name: "Don Syme"
    link: "https://researchr.org/alias/don-syme"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2002"
  doi: "http://link.springer.de/link/service/series/0558/bibs/2514/25140418.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/2514/25140418.htm"
  tags:
  - "type soundness"
  researchr: "https://researchr.org/publication/SymeG02"
  cites: 0
  citedby: 0
  pages: "418-434"
  booktitle: "lpar"
  kind: "inproceedings"
  key: "SymeG02"
- title: "Secrecy and group creation"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Giorgio Ghelli"
    link: "https://researchr.org/alias/giorgio-ghelli"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2005"
  doi: "http://dx.doi.org/10.1016/j.ic.2004.08.003"
  links:
    doi: "http://dx.doi.org/10.1016/j.ic.2004.08.003"
  researchr: "https://researchr.org/publication/CardelliGG05"
  cites: 0
  citedby: 0
  journal: "iandc"
  volume: "196"
  number: "2"
  pages: "127-155"
  kind: "article"
  key: "CardelliGG05"
- title: "A Calculus for Cryptographic Protocols: The spi Calculus"
  author:
  - name: "Martín Abadi"
    link: "https://researchr.org/alias/mart%C3%ADn-abadi"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1999"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/AbadiG99"
  cites: 0
  citedby: 0
  journal: "iandc"
  volume: "148"
  number: "1"
  pages: "1-70"
  kind: "article"
  key: "AbadiG99"
- title: "Mobile ambients"
  author:
  - name: "Luca Cardelli"
    link: "http://lucacardelli.name"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2000"
  doi: "http://dx.doi.org/10.1016/S0304-3975(99)00231-5"
  links:
    doi: "http://dx.doi.org/10.1016/S0304-3975(99)00231-5"
  tags:
  - "mobile"
  researchr: "https://researchr.org/publication/CardelliG00%3A0"
  cites: 0
  citedby: 0
  journal: "TCS"
  volume: "240"
  number: "1"
  pages: "177-213"
  kind: "article"
  key: "CardelliG00:0"
- title: "Guest Editors  Foreword"
  author:
  - name: "Luca Aceto"
    link: "https://researchr.org/alias/luca-aceto"
  - name: "Mario Bravetti"
    link: "https://researchr.org/alias/mario-bravetti"
  - name: "Wan Fokkink"
    link: "http://www.cs.vu.nl/~wanf/"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2008"
  doi: "http://dx.doi.org/10.1016/j.jlap.2007.06.001"
  links:
    doi: "http://dx.doi.org/10.1016/j.jlap.2007.06.001"
  researchr: "https://researchr.org/publication/AcetoBFG08"
  cites: 0
  citedby: 0
  journal: "jlp"
  volume: "75"
  number: "1"
  pages: "1-2"
  kind: "article"
  key: "AcetoBFG08"
- title: "Secure compilation of a multi-tier web language"
  author:
  - name: "Ioannis G. Baltopoulos"
    link: "https://researchr.org/alias/ioannis-g.-baltopoulos"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1481861.1481866"
  links:
    doi: "http://doi.acm.org/10.1145/1481861.1481866"
  researchr: "https://researchr.org/publication/BaltopoulosG09"
  cites: 0
  citedby: 0
  pages: "27-38"
  booktitle: "tldi"
  kind: "inproceedings"
  key: "BaltopoulosG09"
- title: "An advisor for web services security policies"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Greg O Shea"
    link: "https://researchr.org/alias/greg-o-shea"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1103022.1103024"
  links:
    doi: "http://doi.acm.org/10.1145/1103022.1103024"
  tags:
  - "web service"
  - "security"
  - "web services"
  researchr: "https://researchr.org/publication/BhargavanFGO05"
  cites: 0
  citedby: 0
  pages: "1-9"
  booktitle: "sws"
  kind: "inproceedings"
  key: "BhargavanFGO05"
- title: "Stack inspection: Theory and variants"
  author:
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/641909.641912"
  links:
    doi: "http://doi.acm.org/10.1145/641909.641912"
  researchr: "https://researchr.org/publication/FournetG03"
  cites: 0
  citedby: 0
  journal: "TOPLAS"
  volume: "25"
  number: "3"
  pages: "360-399"
  kind: "article"
  key: "FournetG03"
- title: "Service Combinators for Farming Virtual Machines"
  author:
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Iman Narasamdya"
    link: "https://researchr.org/alias/iman-narasamdya"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-540-68265-3_3"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-68265-3_3"
  researchr: "https://researchr.org/publication/BhargavanGN08"
  cites: 0
  citedby: 0
  pages: "33-49"
  booktitle: "coordination"
  kind: "inproceedings"
  key: "BhargavanGN08"
- title: "Authenticity by Typing for Security Protocols"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Alan Jeffrey"
    link: "https://researchr.org/alias/alan-jeffrey"
  year: "2001"
  doi: "http://csdl.computer.org/comp/proceedings/csfw/2001/1146/00/11460145abs.htm"
  links:
    doi: "http://csdl.computer.org/comp/proceedings/csfw/2001/1146/00/11460145abs.htm"
  tags:
  - "protocol"
  - "security"
  researchr: "https://researchr.org/publication/GordonJ01%3A0"
  cites: 0
  citedby: 0
  pages: "145-159"
  booktitle: "csfw"
  kind: "inproceedings"
  key: "GordonJ01:0"
- title: "Bisimilarity for a First-Order Calculus of Objects with Subtyping"
  author:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Gareth D. Rees"
    link: "https://researchr.org/alias/gareth-d.-rees"
  year: "1996"
  doi: "http://doi.acm.org/10.1145/237721.237807"
  links:
    doi: "http://doi.acm.org/10.1145/237721.237807"
  tags:
  - "meta-model"
  - "subtyping"
  - "Meta-Environment"
  - "meta-objects"
  researchr: "https://researchr.org/publication/GordonR96"
  cites: 0
  citedby: 0
  pages: "386-395"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "GordonR96"
- title: "Semantic subtyping with an SMT solver"
  author:
  - name: "Gavin M. Bierman"
    link: "https://researchr.org/alias/gavin-m.-bierman"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "Catalin Hritcu"
    link: "https://researchr.org/alias/catalin-hritcu"
  - name: "David E. Langworthy"
    link: "https://researchr.org/alias/david-e.-langworthy"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863560"
  abstract: "We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, interpreting types as formulas allows us to call the SMT solver at run-time to compute instances of types. "
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863560"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/BiermanGHL10"
  tags:
  - "semantics"
  - "model checking"
  - "meta-model"
  - "modeling language"
  - "refinement"
  - "language modeling"
  - "testing"
  - "subtyping"
  - "type checking"
  - " algebra"
  - "logic"
  - "type theory"
  - "Meta-Environment"
  - "domain-specific language"
  researchr: "https://researchr.org/publication/BiermanGHL10"
  cites: 0
  citedby: 0
  pages: "105-116"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "BiermanGHL10"
- title: "A Bisimulation Method for Cryptographic Protocols"
  author:
  - name: "Martín Abadi"
    link: "http://users.soe.ucsc.edu/~abadi/home.html"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  year: "1998"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1381/13810012.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1381/13810012.htm"
  tags:
  - "protocol"
  researchr: "https://researchr.org/publication/AbadiG98"
  cites: 0
  citedby: 0
  pages: "12-26"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "AbadiG98"
- title: "Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings"
  year: "2003"
  tags:
  - "e-science"
  researchr: "https://researchr.org/publication/fossacs%3A2003"
  cites: 0
  citedby: 0
  booktitle: "Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings"
  conference: "fossacs"
  editor:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  volume: "2620"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-00897-7"
  kind: "proceedings"
  key: "fossacs:2003"
- title: "Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-11957-6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-11957-6"
  tags:
  - "programming languages"
  - "programming"
  researchr: "https://researchr.org/publication/esop-2010"
  cites: 0
  citedby: 0
  booktitle: "Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings"
  conference: "ESOP"
  editor:
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  volume: "6012"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-11956-9"
  kind: "proceedings"
  key: "esop-2010"
- title: "Proceedings of the 2006 ACM workshop on Formal methods in security engineering, FMSE 2006, Alexandria, VA, USA, November 3, 2006"
  year: "2006"
  tags:
  - "security"
  researchr: "https://researchr.org/publication/ccs%3A2006fmse"
  cites: 0
  citedby: 0
  booktitle: "Proceedings of the 2006 ACM workshop on Formal methods in security engineering, FMSE 2006, Alexandria, VA, USA, November 3, 2006"
  editor:
  - name: "Marianne Winslett"
    link: "https://researchr.org/alias/marianne-winslett"
  - name: "Andrew D. Gordon"
    link: "http://research.microsoft.com/en-us/um/people/adg/"
  - name: "David Sands"
    link: "https://researchr.org/alias/david-sands"
  publisher: "ACM"
  isbn: "1-59593-550-9"
  kind: "proceedings"
  key: "ccs:2006fmse"