Andrew D. Gordon

Andrew D. Gordon, Mihhail Aizatulin, Johannes Borgström, Guillaume Claret, Thore Graepel, Aditya V. Nori, Sriram K. Rajamani, Claudio V. Russo: A model-learner pattern for bayesian reasoning. POPL 2013: 403-416

Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio V. Russo: Deriving Probability Density Functions from Probabilistic Functional Programs. TACAS 2013: 508-522

Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy: Semantic subtyping with an SMT solver. J. Funct. Program. 22(1): 31-105 (2012)

Mihhail Aizatulin, Andrew D. Gordon, Jan Jürjens: Computational verification of C protocol implementations by symbolic execution. ACM Conference on Computer and Communications Security 2012: 712-723

Johannes Borgström, Andrew D. Gordon, Riccardo Pucella: Roles, stacks, histories: A triple for Hoare. J. Funct. Program. 21(2): 159-207 (2011)

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2): 8 (2011)

Mihhail Aizatulin, Andrew D. Gordon, Jan Jürjens: Extracting and verifying cryptographic models from C protocol code by symbolic execution. ACM Conference on Computer and Communications Security 2011: 331-340

François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann: Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CSF 2011: 3-17

Ioannis G. Baltopoulos, Johannes Borgström, Andrew D. Gordon: Maintaining Database Integrity with Refinement Types. ECOOP 2011: 484-509

Johannes Borgström, Andrew D. Gordon, Michael Greenberg, James Margetson, Jurgen Van Gael: Measure Transformer Semantics for Bayesian Machine Learning. ESOP 2011: 77-96

Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon: Cryptographic Verification by Typing for a Sample Protocol Implementation. FOSAD 2011: 66-100

Mihhail Aizatulin, François Dupressoir, Andrew D. Gordon, Jan Jürjens: Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. Formal Aspects in Security and Trust 2011: 1-20

Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell: Robin Milner 1934--2010: verification, languages, and concurrency. POPL 2011: 473-474

Mihhail Aizatulin, Andrew D. Gordon, Jan Jürjens: Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution. CoRR abs/1107.1017 (2011)

Moritz Y. Becker, Cédric Fournet, Andrew D. Gordon: SecPAL: Design and semantics of a decentralized authorization language. Journal of Computer Security 18(4): 619-665 (2010)

Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy: Semantic subtyping with an SMT solver. ICFP 2010: 105-116

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon: Modular verification of security protocol code by typing. POPL 2010: 445-456

Andrew D. Gordon, Cédric Fournet: Principles and Applications of Refinement Types. Logics and Languages for Reliability and Security 2010: 73-104

Andrew D. Gordon (Ed.): 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. Lecture Notes in Computer Science 6012, Springer 2010, isbn 978-3-642-11956-9

Andrew D. Gordon, Hans Hüttel, René Rydhof Hansen: Type Inference for Correspondence Types. Electr. Notes Theor. Comput. Sci. 242(3): 21-36 (2009)

Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon: A compositional theory for STM Haskell. Haskell 2009: 69-80

Aybek Mukhamedov, Andrew D. Gordon, Mark Ryan: Towards a Verified Reference Implementation of a Trusted Platform Module. Security Protocols Workshop 2009: 69-81

Ioannis G. Baltopoulos, Andrew D. Gordon: Secure compilation of a multi-tier web language. TLDI 2009: 27-38

Johannes Borgström, Andrew D. Gordon, Andrew Phillips: A Chart Semantics for the Pi-Calculus. Electr. Notes Theor. Comput. Sci. 194(2): 3-29 (2008)

Luca Aceto, Mario Bravetti, Wan Fokkink, Andrew D. Gordon: Guest Editors' Foreword. J. Log. Algebr. Program. 75(1): 1-2 (2008)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon: Verifying policy-based web services security. ACM Trans. Program. Lang. Syst. 30(6) (2008)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse: Verified interoperable implementations of security protocols. ACM Trans. Program. Lang. Syst. 31(1) (2008)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy: Verified implementations of the information card federated identity-management protocol. ASIACCS 2008: 123-135

Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya: Service Combinators for Farming Virtual Machines. COORDINATION 2008: 33-49

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis: Refinement Types for Secure Implementations. CSF 2008: 17-32

Sergio Maffeis, Martín Abadi, Cédric Fournet, Andrew D. Gordon: Code-Carrying Authorization. ESORICS 2008: 563-579

Luca Aceto, Mario Bravetti, Wan Fokkink, Andrew D. Gordon: Guest Editors' Foreword. J. Log. Algebr. Program. 70(2): 119-120 (2007)

Luca Aceto, Mario Bravetti, Wan Fokkink, Andrew D. Gordon: Guest Editors' Foreword. J. Log. Algebr. Program. 72(1): 1-2 (2007)

Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon: Secure sessions for Web services. ACM Trans. Inf. Syst. Secur. 10(2) (2007)

Cédric Fournet, Andrew D. Gordon, Sergio Maffeis: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5) (2007)

Moritz Y. Becker, Cédric Fournet, Andrew D. Gordon: Design and Semantics of a Decentralized Authorization Language. CSF 2007: 3-15

Cédric Fournet, Andy Gordon, Sergio Maffeis: A Type Discipline for Authorization in Distributed Systems. CSF 2007: 31-48

Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya: Service Combinators for Farming Virtual Machines. TGC 2007: 22

Luca Aceto, Andrew D. Gordon: Preface. Electr. Notes Theor. Comput. Sci. 162: 1-2 (2006)

Andrew D. Gordon: V for Virtual. Electr. Notes Theor. Comput. Sci. 162: 177-181 (2006)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse: Verified Interoperable Implementations of Security Protocols. CSFW 2006: 139-152

Andrew D. Gordon: Provable Implementations of Security Protocols. LICS 2006: 345-346

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon: Verified Reference Implementations of WS-Security Protocols. WS-FM 2006: 88-106

Marianne Winslett, Andrew D. Gordon, David Sands (Eds.): Proceedings of the 2006 ACM workshop on Formal methods in security engineering, FMSE 2006, Alexandria, VA, USA, November 3, 2006. ACM 2006, isbn 1-59593-550-9

Andrew D. Gordon, Riccardo Pucella: Validating a web service security abstraction by typing. Formal Asp. Comput. 17(3): 277-318 (2005)

Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon: Secrecy and group creation. Inf. Comput. 196(2): 127-155 (2005)

Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon: Deciding validity in a spatial logic for trees. J. Funct. Program. 15(4): 543-572 (2005)

Andrew D. Gordon: Preface for the Special Issue: Foundations of Software Science and Computation Structures. Theor. Comput. Sci. 333(1-2): 1 (2005)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon: A semantics for web services authentication. Theor. Comput. Sci. 340(1): 102-153 (2005)

Andrew D. Gordon, Alan Jeffrey: Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus. CONCUR 2005: 186-201

Cédric Fournet, Andrew D. Gordon, Sergio Maffeis: A Type Discipline for Authorization Policies. ESOP 2005: 141-156

Andrew D. Gordon: From Typed Process Calculi to Source-Based Security. SAS 2005: 2

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea: An advisor for web services security policies. SWS 2005: 1-9

Andrew D. Gordon, Alan Jeffrey: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security 12(3-4): 435-483 (2004)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon: Verifying policy-based security for web services. ACM Conference on Computer and Communications Security 2004: 268-277

Frédéric Besson, Tomasz Blanc, Cédric Fournet, Andrew D. Gordon: From Stack Inspection to Access Control: A Security Analysis for Libraries. CSFW 2004: 61-

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon: A semantics for web services authentication. POPL 2004: 198-209

Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon: Secure sessions for web services. SWS 2004: 56-66

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella: TulaFale: A Security Tool for Web Services. CoRR abs/cs/0412044 (2004)

Andrew D. Gordon, Riccardo Pucella: Validating a Web Service Security Abstraction by Typing. CoRR abs/cs/0412045 (2004)

Andrew D. Gordon, Alan Jeffrey: Authenticity by Typing for Security Protocols. Journal of Computer Security 11(4): 451-520 (2003)

Andrew D. Gordon, Luca Cardelli: Equational Properties Of Mobile Ambients. Mathematical Structures in Computer Science 13(3): 371-408 (2003)

Andrew D. Gordon, Alan Jeffrey: Typing correspondence assertions for communication protocols. Theor. Comput. Sci. 300(1-3): 379-409 (2003)

Witold Charatonik, Silvano Dal-Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot: Model checking mobile ambients. Theor. Comput. Sci. 308(1-3): 277-331 (2003)

Cédric Fournet, Andrew D. Gordon: Stack inspection: Theory and variants. ACM Trans. Program. Lang. Syst. 25(3): 360-399 (2003)

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella: TulaFale: A Security Tool for Web Services. FMCO 2003: 197-222

Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon: Deciding validity in a spatial logic for trees. TLDI 2003: 62-73

Andrew D. Gordon (Ed.): 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. Lecture Notes in Computer Science 2620, Springer 2003, isbn 3-540-00897-7

Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon: Types for the Ambient Calculus. Inf. Comput. 177(2): 160-194 (2002)

Silvano Dal-Zilio, Andrew D. Gordon: Region analysis and a pi-calculus with groups. J. Funct. Program. 12(3): 229-292 (2002)

Andrew D. Gordon: Types for Cryptographic Protocols. CONCUR 2002: 99-100

Andrew D. Gordon, Alan Jeffrey: Types and Effects for Asymmetric Cryptographic Protocols. CSFW 2002: 77-91

Witold Charatonik, Andrew D. Gordon, Jean-Marc Talbot: Finite-Control Mobile Ambients. ESOP 2002: 295-313

Andy Gordon: Authenticity Types for Cryptographic Protocols. FASec 2002: 3

Andrew D. Gordon: XML Web Services: The Global Computer? IFIP TCS 2002: 355

Andrew D. Gordon, Alan Jeffrey: Typing One-to-One and One-to-Many Correspondences in Security Protocols. ISSS 2002: 263-282

Don Syme, Andrew D. Gordon: Automating Type Soundness Proofs via Decision Procedures and Guided Reductions. LPAR 2002: 418-434

Cédric Fournet, Andrew D. Gordon: Stack inspection: theory and variants. POPL 2002: 307-318

Andrew D. Gordon, Riccardo Pucella: Validating a Web service security abstraction by typing. XML Security 2002: 18-29

Andrew D. Gordon, Alan Jeffrey: Typing Correspondence Assertions for Communication Protocols. Electr. Notes Theor. Comput. Sci. 45: 119-140 (2001)

Andrew D. Gordon, Alan Jeffrey: Authenticity by Typing for Security Protocols. CSFW 2001: 145-159

Witold Charatonik, Silvano Dal-Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot: The Complexity of Model Checking Mobile Ambients. FoSSaCS 2001: 152-167

Andrew D. Gordon, Don Syme: Typing a multi-language intermediate code. POPL 2001: 248-260

Andrew D. Gordon: Types for Cyphers: Thwarting Mischief and Malice with Type Theory. PPDP 2001: 136

Andrew D. Gordon, Alan Jeffrey: A Type and Effect Analysis of Security Protocols. SAS 2001: 432-432

Luca Cardelli, Andrew D. Gordon: Logical Properties of Name Restriction. TLCA 2001: 46-60

Luca Cardelli, Andy Gordon, Giorgio Ghelli: Secrecy, Group Creation. Electr. Notes Theor. Comput. Sci. 40: 7 (2000)

Luca Cardelli, Andrew D. Gordon: Mobile ambients. Theor. Comput. Sci. 240(1): 177-213 (2000)

Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon: Secrecy and Group Creation. CONCUR 2000: 365-379

Andrew D. Gordon: Notes on Nominal Calculi for Security and Mobility. FOSAD 2000: 262-330

Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon: Ambient Groups and Mobility Types. IFIP TCS 2000: 333-347

Silvano Dal-Zilio, Andrew D. Gordon: Region Analysis and a pi-Calculus wiht Groups. MFCS 2000: 1-20

Luca Cardelli, Andrew D. Gordon: Anytime, Anywhere: Modal Logics for Mobile Ambients. POPL 2000: 365-377

Andrew D. Gordon, Andrew M. Pitts: Preface. Electr. Notes Theor. Comput. Sci. 26: 1-2 (1999)

Martín Abadi, Andrew D. Gordon: A Calculus for Cryptographic Protocols: The spi Calculus. Inf. Comput. 148(1): 1-70 (1999)

Andrew D. Gordon, Paul D. Hankin, Søren B. Lassen: Compilation and Equivalence of Imperative Objects. J. Funct. Program. 9(4): 373-426 (1999)

Roy L. Crole, Andrew D. Gordon: Relating operational and denotational semantics for input/output effects. Mathematical Structures in Computer Science 9(2): 125-158 (1999)

Andrew D. Gordon: Bisimilarity as a Theory of Functional Programming. Theor. Comput. Sci. 228(1-2): 5-47 (1999)

Andrew D. Gordon, Luca Cardelli: Equational Properties of Mobile Ambients. FoSSaCS 1999: 212-226

Luca Cardelli, Andrew D. Gordon, Giorgio Ghelli: Mobility Types for Mobile Ambients. ICALP 1999: 230-239

Luca Cardelli, Andrew D. Gordon: Types for Mobile Ambients. POPL 1999: 79-92

Andrew D. Gordon, Paul D. Hankin: A Concurrent Object Calculus: Reduction and Typing. Electr. Notes Theor. Comput. Sci. 16(3): 248-264 (1998)

Martín Abadi, Andrew D. Gordon: A Bisimulation Method for Cryptographic Protocols. Nord. J. Comput. 5(4): 267- (1998)

Martín Abadi, Andrew D. Gordon: A Bisimulation Method for Cryptographic Protocols. ESOP 1998: 12-26

Luca Cardelli, Andrew D. Gordon: Mobile Ambients. FoSSaCS 1998: 140-155

Andrew D. Gordon, Andrew M. Pitts, Carolyn L. Talcott: Preface. Electr. Notes Theor. Comput. Sci. 10: 1 (1997)

Luca Cardelli, Andrew D. Gordon: Mobile Ambients. Electr. Notes Theor. Comput. Sci. 10: 198-201 (1997)

Martín Abadi, Andrew D. Gordon: A Calculus for Cryptographic Protocols: The Spi Calculus. ACM Conference on Computer and Communications Security 1997: 36-47

Martín Abadi, Andrew D. Gordon: Reasoning about Cryptographic Protocols in the Spi Calculus. CONCUR 1997: 59-73

Andrew D. Gordon, Paul D. Hankin, Søren B. Lassen: Compilation and Equivalence of Imperative Objects. FSTTCS 1997: 74-87

Simon L. Peyton Jones, Andrew D. Gordon, Sigbjorn Finne: Concurrent Haskell. POPL 1996: 295-308

Andrew D. Gordon, Gareth D. Rees: Bisimilarity for a First-Order Calculus of Objects with Subtyping. POPL 1996: 386-395

Andrew D. Gordon, Thomas F. Melham: Five Axioms of Alpha-Conversion. TPHOLs 1996: 173-190

Andrew D. Gordon: Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci. 1: 232-252 (1995)

Roy L. Crole, Andrew D. Gordon: A Sound Metalogical Semantics for Input/Output Effects. CSL 1994: 339-353

Andrew D. Gordon: An Operational Semantics for I/O in a Lazy Functional Language. FPCA 1993: 136-145

Andrew D. Gordon: A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. HUG 1993: 413-425

Andrew D. Gordon: The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic. ICCD 1992: 531-534

Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel: Experience with Embedding Hardware Description Languages in HOL. TPCD 1992: 129-156