Andrew D. Gordon: Some Talks

Experience with Verifying Cryptographic Software in C

(OWASP Edinburgh, February 2012) [PDF]

Progress on Provable Implementations of Security Protocols

(Engineering Secure Software and Systems (ESSoS’10), Pisa, February 2010) [PDF]

Modular Verification of Security Protocol Code by Typing

(ACM POPL 2010, Madrid, January 2010) [PDF]

Some Challenges for Future ITP

(Workshop on Interactive Theorem Proving, University of Cambridge, August 2009) [PDF]

Modular Verification of Security Protocol Code by Typing

(ACM SIGPLAN Workshop on ML, Edinburgh, August 2009) [PDF]

Principles and Applications of Refinement Types

(Lectures at the 30th International Summer School Marktoberdorf, August 4-16, 2009) [PDF]

Rigorous Security Analysis of Software

(Panel statement at CSF 2009, July 8-10, 2009) [PDF]

Roles, Stacks, Histories: A Triple for Hoare

(Celebrating the Work of Sir Tony Hoare, April 16-17, 2009) [PDF]

V for Virtual

            (Lab Tutorial, MSR Cambridge, October 4, 2007) [PDF]

Security Types for F#

(Jesper Bengtson’s end of internship talk, MSR Cambridge, July 25, 2007) [PDF]

A Type Discipline for Authorization in Distributed Systems

(Talk at CSF 2007, Venice, July 6-8, 2007) [PDF]

From Typed Process Calculi to Source-Based Security

(Invited talk at SAS 2005, London, September 7-9, 2005) [PowerPoint]

Web Services and Security

(Fourth International Sumer School on Foundations of Security Analysis and Design (FOSAD 2004) at University Residential Centre in Bertinoro, September 6-11, 2004)  [PDF]

Secure Global Computing with XML Web Services: Theory and Practice

(EEF Global Computing Summer School, Edinburgh, July 7-11, 2003)  [PDF]

A Calculus for Cryptographic Protocols

(Summer School on Foundations of Internet Security, June 14-23, 2002, Duszniki Zdrój, Poland) [PDF]

Types and Effects for Asymmetric Cryptographic Protocols

(Imperial College, March 2002) [Powerpoint]

Typing a Multilanguage Intermediate Code

(University of Sussex, February 2001) [Zipped PostScript]

Nominal Calculi for Security and Mobility

(International Summer School on Foundations of Security Analysis and Design (FOSAD 2000) at University Residential Centre in Bertinoro, September 18-30, 2000) Parts I and II (pi and spi) [PostScript,HTML] Part III (ambients) [PDF] Lecture notes are available here.  Parts I and II were updated for the Polish school of June 2002.

Name Groups and Group Creation: Semantics and Applications

(MFPS 16, Hoboken, April 2000) [A4 gzip'd PostScript, PDF]

A Typed Calculus of Mobile Computation

(Workshop on Foundations of Mobile Computation, Chennai, December 1999) [A4 zip'd PostScript, PDF]

Anytime, Anywhere: Modal Logics for Mobile Ambients

(University of Sussex, May 1999) [PDF]

Equational Properties of Mobile Ambients

(FoSSaCS'99, Amsterdam, March 1999) [PDF]

Types for Mobile Ambients

(AppSem'98, Pisa, September 1998) [PostScript, PDF]

A Concurrent Object Calculus

(HLCL'98, Nice, September 1998) [PostScript, PDF]

Semantics and Types of Mobile Ambients

(MathFit Instruction Meeting on Semantics and Types for Concurrency, Imperial College, July 1998) [PostScript, PDF]

From Programming Features to Fragmental Calculi

(Semantics Lunch, University of Cambridge, October 1997) [A4 gzip'd PostScript]

A Calculus of Mobile Ambients

(INRIA, Paris, May 1997) [PDF]

A Calculus for Cryptographic Protocols: The Spi Calculus

(WG2.8, Lake Mohonk, September 1996) [US Letter gzip'd PostScript]

Five Axioms of Alpha-Conversion

(SRI, Menlo Park, August 1996) [A4 gzip'd PostScript]

An Operational Theory of Objects

(University of Birmingham, June 1996) [A4 gzip'd PostScript]