Andrew D. Gordon: Publications

Cryptographic Verification by Typing for a Sample Protocol Implementation.

(With C. Fournet and K. Bhargavan, FOSAD 2010) [Details]

Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution.

(With M. Aizatulin and J. Jürjens, CCS 2011) [Details]

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.

(With F. Dupressoir, J. Jürjens, and D. Naumann, CSF 2011) [Details]

Maintaining database integrity with refinement types.

(With I. Baltopoulos and J. Borgström, ECOOP 2011) [Details]

Measure transformer semantics for Bayesian machine learning.

(With J. Borgström, M. Greenberg, J. Margetson, and J. Van Gael, ESOP 2011) [Details]

Robin Milner 1934 – 2010: Verification, Languages, and Concurrency.

(With R. Harper, J. Harrison, A. Jeffrey, and P. Sewell, POPL 2011) [Details]

Semantic subtyping with an SMT solver.

(With G. Bierman, C. Hriţcu, and D. Langworthy, ICFP 2010) [Details]

Programming Languages and Systems: 19th European Symposium on Programming (ESOP 2010)

(Editor) [Details]

Modular verification of security protocol code by typing

(With K. Bhargavan and C. Fournet, POPL 2010) [Details]

Principles and applications of refinement types

(With C. Fournet. Marktoberdorf Summer School Symposium 2009) [Details]

A Compositional Theory for STM Haskell.

(With J. Borgström and K. Bhargavan. Haskell Symposium 2009) [Details]

Roles, stacks, histories: a triple for Hoare

(With J. Borgström and R. Pucella. Hoare Festschrift Volume, 2009) [Details]

Towards a verified reference implementation of a Trusted Platform Module

(With A. Mukhamedov and M. Ryan.  Security Protocols Workshop 2009) [Details]

Secure compilation of a multi-tier web language

(With I. Baltopoulos. TLDI’09) [Details]

Code-carrying authorization

(With S. Maffeis, M. Abadi, and C. Fournet. ESORICS’08) [Details]

Type inference for correspondence types

(With H. Huettel and R. Rydhof Hansen. SecCo’08) [Details]

Refinement types for secure implementations

(With J. Bengtson, K. Bhargavan, C. Fournet, and S. Maffeis. CSF’08) [Details]

Service combinators for farming virtual machines

(With K. Bhargavan and I. Narasamdya. COORDINATION’08) [Details]

Getting operations logic right: types, service-orientation, and static analysis

(With K. Bhargavan. Rise and Rise of the Declarative Datacentre, 2008) [Details]

Rise and Rise of the Declarative Datacentre

(Co-editor with K. Bhargavan, T. Harris, and P. Toft. MSR TR-2008-61) [Details]

Verified implementations of the Information Card federated identity-management protocol

(With K. Bhargavan, C. Fournet, and N. Swamy. ASIACCS’08) [Details]

A chart semantics for the pi-calculus

(With J. Borgström and A. Phillips. EXPRESS'07) [Details]

A type system for authorization in distributed systems

(With C. Fournet and S. Maffeis. CSF’07) [Details]

Design and semantics of a decentralised authorization language

(With M. Becker and C. Fournet. CSF’07) [Details]

Verified reference implementations of WS-Security protocols

(With K. Bhargavan and C. Fournet. WSFM'06) [Details]

Provable implementations of security protocols

(LICS'06) [Details]

Verified interoperable implementations of security protocols

(With K. Bhargavan, C. Fournet, and S. Tse. CSFW'06) [Details]

Policy Advisor for WSE 3

(With K. Bhargavan and C. Fournet. WSE Patterns and Guidance, 2006) [Details]

An advisor for web services security policies

(With K. Bhargavan, C. Fournet, and G. O'Shea. SWS'05) [Details]

Algebraic Process Calculi: The First Twenty Five Years and Beyond

(Co-editor with L. Aceto. BRICS Note NS-05-03) [Details]

Secrecy despite compromise: types, cryptography, and the pi-calculus

(With A. Jeffrey. CONCUR'05) [Details]

Foundations of Software Science and Computation Structures

(Editor. TCS Volume 333) [Details]

A type discipline for authorization policies

(With C. Fournet and S. Maffeis. ESOP'05) [Details]

Secure sessions for web services

(With K. Bhargavan, R. Corin, and C. Fournet. SWS'04) [Details]

Verifying Policy-Based Security for Web Services

(With K. Bhargavan and C. Fournet. CCS'04) [Details]

TulaFale: A security tool for web services

(With K. Bhargavan, C. Fournet, and R. Pucella. FMCO'03) [Details]

From stack inspection to access control: A security analysis for libraries

(With F. Besson, T. Blanc, and C. Fournet. CSFW'04) [Details]

A semantics for web services authentication

(With K. Bhargavan and C. Fournet. POPL'04) [Details]

Foundations of Software Science and Computation Structures (FOSSACS 2003)

(Editor) [Details]

Deciding validity in a spatial logic for trees

(With C. Calcagno and L. Cardelli. TLDI 2003) [Details]

Validating a web service security abstraction by typing

(With R. Pucella. XML Security, 2002) [Details]

Typing one-to-one and one-to-many correspondences in security protocols

(With A. Jeffrey. ISSS, 2002) [Details]

Automating type soundness proofs via decision procedures and guided reductions

(With D. Syme. LPAR, 2002) [Details]

Types and effects for asymmetric cryptographic protocols

(With A. Jeffrey. CSFW, 2002) [Details]

Finite-control mobile ambients

(With W. Charatonik and J.-M. Talbot.  ESOP'02) [Details]

Stack inspection: theory and variants

(With C. Fournet. POPL'02) [Details]

Types for the ambient calculus

(With L. Cardelli and G. Ghelli. Collation of material presented at POPL99, ICALP'99, and TCS 2000) [Details]

Notes on nominal calculi for security and mobility

(FOSAD book, 2002) [Details]

Authenticity by typing for security protocols

(With A. Jeffrey. CSFW, 2001) [Details]

Typing correspondence assertions for communication protocols

(With A. Jeffrey. MFPS, 2001) [Details]

Logical properties of name restriction

(With L. Cardelli. TLCA'01) [Details]

The complexity of model checking mobile ambients

(With W. Charatonik, S. Dal Zilio, S. Mukhopadhyay, and J.-M. Talbot.  FOSSACS'01) [Details]

Typing a multilanguage intermediate code

(With D. Syme.  POPL'01) [Details]

A commitment relation for the ambient calculus

(With L. Cardelli. Note, 2000) [Details]

Region analysis and a p-calculus with groups

(With S. Dal Zilio. MFCS'00) [Details]

Secrecy and group creation

(With L. Cardelli and G. Ghelli. CONCUR 2000) [Details]

Ambient groups and mobility types

(With L. Cardelli and G. Ghelli. TCS2000) [Details]

Anytime, anywhere: modal logics for mobile ambients

(With L. Cardelli. POPL'00) [Details]

Mobility types for mobile ambients

(With L. Cardelli and G. Ghelli. ICALP'99) [Details]

Equational properties of mobile ambients

(With L. Cardelli. FOSSACS'99) [Details]

Types for mobile ambients

(With L. Cardelli. POPL'99) [Details]

A concurrent object calculus: reduction and typing

(With P. D. Hankin, HLCL'98) [Details]

A bisimulation method for cryptographic protocols

(With M. Abadi. ESOP'98) [Details]

Mobile ambients

(With L. Cardelli. FOSSACS'98) [Details]

A calculus for cryptographic protocols: the spi calculus

(With M. Abadi. Information and Computation, 148:1-70 (1999)) [Details]

Operational equivalences for untyped and polymorphic object calculi

(HOOTS book, 1998) [Details]

Higher Order Operational Techniques in Semantics

(Editor with Andrew M. Pitts. CUP, 1998) [Details]

Compilation and equivalence of imperative objects

(With P. D. Hankin and S. B. Lassen. FST&TCS'97) [Details]

Reasoning about cryptographic protocols in the spi calculus

(With M. Abadi. CONCUR'97) [Details]

A calculus for cryptographic protocols: the spi calculus

(With M. Abadi. CCS'97) [Details]

Nominal calculi for security and mobility

(FSMC'97) [Details]

Five axioms of alpha-conversion

(With T.F. Melham. HUG'96) [Details]

The Haskell language report, version 1.3

(With others. Yale, 1996) [Details] [HTML]

The Haskell library report, version 1.3

(With others. Yale, 1996) [Details] [HTML]

Book review

(JFP, 1996) [Details]

Concurrent Haskell

(With S. Peyton Jones and S. Finne. POPL'96) [Details]

Bisimilarity for a first-order calculus of objects with subtyping

(With G.D. Rees. POPL'96) [Details]

A HOL embedding of a small parallel HDL.

(With M. Larson. HUG'95)

Monadic I/O in Haskell 1.3.

(With K. Hammond. Haskell'95) [Details]

Bisimilarity as a theory of functional programming.

(MFPS'95) [Details]

A tutorial on co-induction and functional programming.

(Glasgow FP'94) [Details]

A sound metalogical semantics for input/output effects.

(With R.L. Crole. CSL'94) [Details]

A mechanisation of name-carrying syntax up to alpha-conversion.

(HUG'93) [Details]

Factoring an adequacy proof (preliminary report).

(With R.L. Crole. Glasgow FP'93) [Details]

An operational semantics for I/O in a lazy functional language.

(FPCA'93) [Details]

Example: the binomial theorem.

(HOL book, CUP, 1993) [Details]

The formal definition of a synchronous hardware-description language in higher order logic.

(ICCD'92) [Details]

Experience with embedding hardware description languages in HOL.

(With R. Boulton, M. Gordon, J. Harrison, J. Herbert, J. Van Tassell. TPCD'92) [Details]

Functional Programming and Input/Output.

(PhD dissertation, Cambridge, 1992; CUP, 1994) [Details]