Martín Abadi
Martín Abadi has been at Google since November 2014.
A list of publications (going back to 1985) and other information is in web pages at UC Santa Cruz (where he is now Emeritus).
Authored Publications
Google Publications
Other Publications
Sort By
Dynamic Control Flow in Large-Scale Machine Learning
Yuan Yu
Eugene Brevdo
Mike Burrows
Tim Harley
Peter Hawkins
Manjunath Kudlur
Rajat Monga
Xiaoqiang Zheng
Proceedings of EuroSys 2018
Preview abstract
Many recent machine learning models rely on fine-grained dynamic control flow for training and inference. In particular, models based on recurrent neural networks and on reinforcement learning depend on recurrence relations, data-dependent conditional execution, and other features that call for dynamic control flow. These applications benefit from the ability to make rapid control-flow decisions across a set of computing devices in a distributed system. For performance, scalability, and expressiveness, a machine learning system must support dynamic control flow in distributed and heterogeneous environments.
This paper presents a programming model for distributed machine learning that supports dynamic control flow. We describe the design of the programming model, and its implementation in TensorFlow, a distributed machine learning system. Our approach extends the use of dataflow graphs to represent machine learning models, offering several distinctive features. First, the branches of conditionals and bodies of loops can be partitioned across many machines to run on a set of heterogeneous devices, including CPUs, GPUs, and custom ASICs. Second, programs written in our model support automatic differentiation and distributed gradient computations, which are necessary for training machine learning models that use control flow. Third, our choice of non-strict semantics enables multiple loop iterations to execute in parallel across machines, and to overlap compute and I/O operations.
We have done our work in the context of TensorFlow, and it has been used extensively in research and production. We evaluate it using several real-world applications, and demonstrate its performance and scalability.
View details
A Computational Model for TensorFlow (An Introduction)
1st ACM SIGPLAN Workshop on Machine Learning and Programming Languages (MAPL 2017) (2017)
Preview abstract
TensorFlow is a powerful, programmable system for machine learning.
This paper aims to provide the basics of a conceptual framework for
understanding the behavior of TensorFlow models during training and inference:
it describes an operational semantics, of the kind common in
the literature on programming languages. More broadly, the paper
suggests that a programming-language perspective is fruitful in
designing and in explaining systems such as TensorFlow.
View details
Preview abstract
We present a method to create universal, robust, targeted adversarial image patches in the real world. The patches are universal because they can be used to attack any scene, robust because they work under a wide variety of transformations, and targeted because they can cause a classifier to output any target class. These adversarial patches can be printed, added to any scene, photographed, and presented to image classifiers; even when the patches are small, they cause the classifiers to ignore the other items in the scene and report a chosen target class.
View details
Preview abstract
We study the interaction of the programming construct ``new'', which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts.
We define the applied pi calculus, a simple, general extension of the pi calculus in which values can be formed from names via the application of built-in functions, subject to equations, and be sent as messages. (In contrast, the pure pi calculus lacks built-in functions; its only messages are atomic names.) We develop semantics and proof techniques for this extended language and apply them in reasoning about security protocols.
This paper essentially subsumes the conference paper that introduced the applied pi calculus in 2001. It fills gaps, incorporates improvements, and further explains and studies the applied pi calculus. Since 2001, the applied pi calculus has been the basis for much further work, described in many research publications and sometimes embodied in useful software, such as the tool ProVerif, which relies on the applied pi calculus to support the specification and automatic analysis of security protocols. Although this paper does not aim to be a complete review of the subject, it benefits from that further work and provides better foundations for some of it. In particular, the applied pi calculus has evolved through its implementation in ProVerif, and the present definition reflects that evolution.
View details
Semi-supervised Knowledge Transfer for Deep Learning from Private Training Data
Nicolas Papernot
Úlfar Erlingsson
Ian Goodfellow
Kunal Talwar
Proceedings of the International Conference on Learning Representations (2017)
Preview abstract
Some machine learning applications involve training data that is sensitive, such as the medical histories of patients in a clinical trial. A model may inadvertently and implicitly store some of its training data; careful analysis of the model may therefore reveal sensitive information.
To address this problem, we demonstrate a generally applicable approach to providing strong privacy guarantees for training data: Private Aggregation of Teacher Ensembles (PATE). The approach combines, in a black-box fashion, multiple models trained with disjoint datasets, such as records from different subsets of users. Because they rely directly on sensitive data, these models are not published, but instead used as “teachers” for a “student” model. The student learns to predict an output chosen by noisy voting among all of the teachers, and cannot directly access an individual teacher or the underlying data or parameters. The student’s privacy properties can be understood both intuitively (since no single teacher and thus no single dataset dictates the student’s training) and formally, in terms of differential privacy. These properties hold even if an adversary can not only query the student but also inspect its internal workings.
Compared with previous work, the approach imposes only weak assumptions on how teachers are trained: it applies to any model, including non-convex models like DNNs. We achieve state-of-the-art privacy/utility trade-offs on MNIST and SVHN thanks to an improved privacy analysis and semi-supervised learning.
View details
Preview abstract
Learning a natural language interface for database tables is a challenging task that involves deep language understanding and multi-step reasoning. The task is often approached by mapping natural language queries to logical forms or programs that provide the desired response when executed on the database. To our knowledge, this paper presents the first weakly supervised, end-to-end neural network model to induce such programs on a real-world dataset. We enhance the objective function of Neural Programmer, a neural network with built-in discrete operations, and apply it on WikiTableQuestions, a natural language question-answering dataset. The model is trained end-to-end with weak supervision of question-answer pairs, and does not require domain-specific grammars, rules, or annotations that are key elements in previous approaches to program induction. The main experimental result in this paper is that a single Neural Programmer model achieves 34.2% accuracy using only 10,000 examples with weak supervision. An ensemble of 15 models, with a trivial combination technique, achieves 37.2% accuracy, which is competitive to the current state-of-the-art accuracy of 37.1% obtained by a traditional natural language semantic parser.
View details
On the Protection of Private Information in Machine Learning Systems: Two Recent Approaches
Úlfar Erlingsson
Ian Goodfellow
Ilya Mironov
Kunal Talwar
Li Zhang
Proceedings of 30th IEEE Computer Security Foundations Symposium (CSF) (2017), pp. 1-6
Preview abstract
The recent, remarkable growth of machine learning has led to intense interest in the privacy of the data on which machine learning relies, and to new techniques for preserving privacy. However, older ideas about privacy may well remain valid and useful. This note reviews two recent works on privacy in the light of the wisdom of some of the early literature, in particular the principles distilled by Saltzer and Schroeder in the 1970s.
View details
Preview abstract
We ask whether neural networks can learn to use secret keys to protect information from other neural networks. Specifically, we focus on ensuring confidentiality properties in a multiagent system, and we specify those properties in terms of an adversary. Thus, a system may consist of neural networks named Alice and Bob, and we aim to limit what a third neural network named Eve learns from eavesdropping on the communication between Alice and Bob. We do not prescribe specific cryptographic algorithms to these neural networks; instead, we train end-to-end, adversarially. We demonstrate that the neural networks can learn how to perform forms of encryption and decryption, and also how to apply these operations selectively in order to meet confidentiality goals.
View details
TensorFlow: A system for large-scale machine learning
Jianmin Chen
Matthieu Devin
Manjunath Kudlur
Rajat Monga
Benoit Steiner
Paul Tucker
Vijay Vasudevan
Pete Warden
Yuan Yu
Xiaoqiang Zheng
12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), USENIX Association (2016), pp. 265-283
Preview abstract
TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. TensorFlow uses dataflow graphs to represent computation, shared state, and the operations that mutate that state. It maps the nodes of a dataflow graph across many machines in a cluster, and within a machine across multiple computational devices, including multicore CPUs, general-purpose GPUs, and custom-designed ASICs known as Tensor Processing Units (TPUs). This architecture gives flexibility to the application developer: whereas in previous “parameter server” designs the management of shared state is built into the system, TensorFlow enables developers to experiment with novel optimizations and training algorithms. TensorFlow supports a variety of applications, with a focus on training and inference on deep neural networks. Several Google services use TensorFlow in production, we have released it as an open-source project, and it has become widely used for machine learning research. In this paper, we describe the TensorFlow dataflow model and demonstrate the compelling performance that Tensor- Flow achieves for several real-world applications.
View details
Deep Learning with Differential Privacy
Andy Chu
Ian Goodfellow
Ilya Mironov
Kunal Talwar
Li Zhang
23rd ACM Conference on Computer and Communications Security (ACM CCS) (2016), pp. 308-318
Preview abstract
Machine learning techniques based on neural networks are achieving remarkable results in a wide variety of domains. Often, the training of models requires large, representative datasets, which may be crowdsourced and contain sensitive information. The models should not expose private information in these datasets. Addressing this goal, we develop new algorithmic techniques for learning and a refined analysis of privacy costs within the framework of differential privacy. Our implementation and experiments demonstrate that we can train deep neural networks with non-convex objectives, under a modest privacy budget, and at a manageable cost in software complexity, training efficiency, and model quality.
View details
TensorFlow: Learning Functions at Scale
ICFP (2016)
Preview abstract
TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. Its computational model is based on dataflow graphs with mutable state. Graph nodes may be mapped to different machines in a cluster, and within each machine to CPUs, GPUs, and other devices. TensorFlow supports a variety of applications, but it particularly targets training and inference with deep neural networks. It serves as a platform for research and for deploying machine learning systems across many areas, such as speech recognition, computer vision, robotics, information retrieval, and natural language processing. In this talk, we describe TensorFlow and outline some of its applications. We also discuss the question of what TensorFlow and deep learning may have to do with functional programming. Although TensorFlow is not purely functional, many of its uses are concerned with optimizing functions (during training), then with applying those functions (during inference). These functions are defined as compositions of simple primitives (as is common in functional programming), with internal data representations that are learned rather than manually designed. TensorFlow is joint work with many other people in the Google Brain team and elsewhere. More information is available at tensorflow.org.
View details
Incremental, iterative data processing with timely dataflow
Frank McSherry
Rebecca Isaacs
Communications of the ACM, vol. 59 (2016), pp. 75-83
Preview abstract
We describe the timely dataflow model for distributed computation and its implementation in the Naiad system. The model supports stateful iterative and incremental computations. It enables both low-latency stream processing and high-throughput batch processing, using a new approach to coordination that combines asynchronous and fine-grained synchronous execution. We describe two of the programming frameworks built on Naiad: GraphLINQ for parallel graph processing, and differential dataflow for nested iterative and incremental computations. We show that a general-purpose system can achieve performance that matches, and sometimes exceeds, that of specialized systems.
View details
Distributed Authorization With Distributed Grammars
Mike Burrows
Himabindu Pucha
Adam Sadovsky
Asim Shankar
Ankur Taly
Programming Languages with Applications to Biology and Security, Springer International Publishing Switzerland, Gewerbestrasse 11 CH-6330 Cham (ZG) Switzerland (2015), pp. 10-26
Preview abstract
While groups are generally helpful for the definition of authorization policies, their use in distributed systems is not straightforward. This paper describes a design for authorization in distributed systems that treats groups as formal languages. The design supports forms of delegation and negative clauses in authorization policies. It also considers the wish for privacy and efficiency in group-membership checks, and the possibility that group definitions may not all be available and may contain cycles.
View details
Preview abstract
This paper studies timely dataflow, a model for data-parallel
computing in which each communication event is associated with a virtual
time. It defines and investigates the could-result-in relation which
is central to this model, then the semantics of timely dataflow graphs.
View details
TensorFlow: Large-Scale Machine Learning on Heterogeneous Distributed Systems
Ashish Agarwal
Eugene Brevdo
Craig Citro
Matthieu Devin
Ian Goodfellow
Andrew Harp
Yangqing Jia
Rafal Jozefowicz
Lukasz Kaiser
Manjunath Kudlur
Dan Mané
Rajat Monga
Chris Olah
Mike Schuster
Jonathon Shlens
Benoit Steiner
Ilya Sutskever
Kunal Talwar
Paul Tucker
Vijay Vasudevan
Pete Warden
Yuan Yu
Xiaoqiang Zheng
tensorflow.org (2015)
Preview abstract
TensorFlow is an interface for expressing machine learning
algorithms, and an implementation for executing such algorithms.
A computation expressed using TensorFlow can be
executed with little or no change on a wide variety of heterogeneous
systems, ranging from mobile devices such as phones
and tablets up to large-scale distributed systems of hundreds
of machines and thousands of computational devices such as
GPU cards. The system is flexible and can be used to express
a wide variety of algorithms, including training and inference
algorithms for deep neural network models, and it has been
used for conducting research and for deploying machine learning
systems into production across more than a dozen areas of
computer science and other fields, including speech recognition,
computer vision, robotics, information retrieval, natural
language processing, geographic information extraction, and
computational drug discovery. This paper describes the TensorFlow
interface and an implementation of that interface that
we have built at Google. The TensorFlow API and a reference
implementation were released as an open-source package under
the Apache 2.0 license in November, 2015 and are available at
www.tensorflow.org.
View details
On the Flow of Data, Information, and Time
Timely Rollback: Specification and Verification
Foundations of Differential Dataflow
The Prophecy of Undo
FASE (2015), pp. 347-361
Web PKI: Closing the Gap between Guidelines and Practices
Antoine Delignat-Lavaud
Andrew Birrell
Ilya Mironov
Ted Wobber
Yinglian Xie
Microsoft Research
NDSS (2014)
Understanding Typescript
Gavin M. Bierman
Mads Torgersen
ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, pp. 257-281
Global Authentication in an Untrustworthy World
On Layout Randomization for Arrays and Functions
Formal Analysis of a Distributed Algorithm for Tracking Progress
SocialWatch: detection of online service abuse via large-scale social graphs
Junxian Huang
Yinglian Xie
Fang Yu
Qifa Ke
Eliot Gillum
Zhuoqing Morley Mao
ASIACCS (2013), pp. 143-148
Message-Locked Encryption for Lock-Dependent Messages
Naiad: a timely dataflow system
Frank McSherry
Rebecca Isaacs
SOSP (2013), pp. 439-455
Early security classification of skype users via machine learning
Layout Randomization and Nondeterminism
Jérémy Planul
Gordon D. Plotkin
Electr. Notes Theor. Comput. Sci., vol. 298 (2013), pp. 29-50
Innocent by association: early recognition of legitimate users
Yinglian Xie
Fang Yu
Qifa Ke
Eliot Gillum
Krish Vitaldevaria
Jason Walter
Junxian Huang
Zhuoqing Morley Mao
ACM Conference on Computer and Communications Security (2012), pp. 353-364
Host Fingerprinting and Tracking on the Web: Privacy and Security Implications
On Protection by Layout Randomization
Software Security: A Formal Perspective - (Notes for a Talk)
FM (2012), pp. 1-5
A Functional View of Imperative Information Flow
Semantics of transactional memory and automatic mutual exclusion
Andrew Birrell
Tim Harris 0001
ACM Trans. Program. Lang. Syst., vol. 33 (2011), pp. 2
Heat-seeking honeypots: design and experience
AC: composable asynchronous IO for native languages
Differential privacy with information flow control
deSEO: Combating Search-Result Poisoning
John P. John
Fang Yu
Yinglian Xie
Arvind Krishnamurthy
USENIX Security Symposium (2011)
A Model of Cooperative Threads
Guessing attacks and the computational soundness of static equivalence
Mathieu Baudet
Bogdan Warinschi
Journal of Computer Security, vol. 18 (2010), pp. 909-968
On Protection by Layout Randomization
The Fine Print of Security
LICS (2010), pp. 110
A model of dynamic separation for transactional memory
Searching the Searchers with SearchAudit
John P. John
Fang Yu
Yinglian Xie
Arvind Krishnamurthy
USENIX Security Symposium (2010), pp. 127-142
How to tell an airport from a home: techniques and applications
Andreas Pitsillidis
Yinglian Xie
Fang Yu
Geoffrey M. Voelker
Stefan Savage
HotNets (2010), pp. 13
A model of cooperative threads
Logic in Access Control (Tutorial Notes)
FOSAD (2009), pp. 145-165
Unified Declarative Platform for Secure Netwoked Information Systems
Implementation and Use of Transactional Memory with Dynamic Separation
Perspectives on Transactional Memory
Control-flow integrity principles, implementations, and applications
De-anonymizing the internet using unreliable IDs
Transactional memory with strong atomicity using off-the-shelf memory protection hardware
Models and Proofs of Protocol Security: A Progress Report
A Model of Dynamic Separation for Transactional Memory
Code-Carrying Authorization
Security analysis of cryptographically controlled access to XML documents
The good, the bad, and the provable
ACM Conference on Computer and Communications Security (2008), pp. 1
Automated verification of selected equivalences for security protocols
Automatic Mutual Exclusion and Atomicity Checks
Concurrency, Graphs and Models (2008), pp. 510-526
A Modal Deconstruction of Access Control Logics
Variations in Access Control Logic
DEON (2008), pp. 96-109
Semantics of transactional memory and automatic mutual exclusion
Policies and Proofs for Code Auditing
Just fast keying in the pi calculus
Editorial
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Towards a Declarative Language and System for Secure Networking
Access Control in a Core Calculus of Dependency
Electr. Notes Theor. Comput. Sci., vol. 172 (2007), pp. 5-31
Security Protocols: Principles and Calculi
FOSAD (2007), pp. 1-23
Authorizing applications in singularity
Ted Wobber
Aydan R. Yumerefendi
Andrew Birrell
Daniel R. Simon
EuroSys (2007), pp. 355-368
Access control in a core calculus of dependency
ICFP (2006), pp. 263-273
Types for safe locking: Static race detection for Java
Cormac Flanagan
Stephen N. Freund
ACM Trans. Program. Lang. Syst., vol. 28 (2006), pp. 207-255
Architectural support for software-based protection
Guessing Attacks and the Computational Soundness of Static Equivalence
Computational Secrecy by Typing for the Pi Calculus
Deciding knowledge in security protocols under equational theories
Secrecy by Typing and File-Access Control
Formal Analysis of Dynamic, Distributed File-System Access Controls
XFI: Software Guards for System Address Spaces
Security analysis of cryptographically controlled access to XML documents
Computer-assisted verification of a protocol for certified email
"Language-Based Security"
Automated Verification of Selected Equivalences for Security Protocols
Control-flow integrity
Mihai Budiu
Úlfar Erlingsson
Jay Ligatti
ACM Conference on Computer and Communications Security (2005), pp. 340-353
A Theory of Secure Control Flow
Moderately hard, memory-bound functions
Michael M. Burrows
Mark Manasse
Ted Wobber
ACM Transactions on Internet Technology, vol. 5 (2005), pp. 299-327
Analyzing security protocols with secrecy types and logic programs
Password-Based Encryption Analyzed
Access Control in a World of Software Diversity
Formal security analysis of basic network-attached storage
Deciding Knowledge in Security Protocols under (Many More) Equational Theories
By Reason and Authority: A System for Authorization of Proof-Carrying Code
Deciding Knowledge in Security Protocols Under Equational Theories
Just Fast Keying in the Pi Calculus
Language-Based Enforcement of Privacy Policies
Choice in Dynamic Linking
Private authentication
BCiC: A System for Code Authentication and Verification
A Logical Account of NGSCB
Trusted Computing, Trusted Third Parties, and Verified Communications
SEC (2004), pp. 291-308
Reasoning About Secrecy for Active Networks
Bankable Postage for Network Services
Logic in Access Control
LICS (2003), pp. 228-
Access Control Based on Execution History
Secrecy types for asymmetric communication
Computer-Assisted Verification of a Protocol for Certified Email
A Logic of Object-Oriented Programs
Built-in Object Security
ECOOP (2003), pp. 1
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Certified email with a light on-line trusted third party: design and implementation
Private Authentication
Privacy Enhancing Technologies (2002), pp. 27-40
Analyzing security protocols with secrecy types and logic programs
Editorial
Secure Implementation of Channel Abstractions
Hiding Names: Private Authentication in the Applied Pi Calculus
Formal Eavesdropping and Its Computational Interpretation
Leslie Lamport's properties and actions
PODC (2001), pp. 15
Computing Symbolic Models for Verifying Cryptographic Protocols
Mobile values, new names, and secure communication
Secrecy Types for Asymmetric Communication
top-top-closed relations and admissibility
Mathematical Structures in Computer Science, vol. 10 (2000), pp. 313-320
Authentication Primitives and Their Compilation
Reasoning about Secrecy for Active Networks
Taming the Adversary
CRYPTO (2000), pp. 353-358
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Object Types against Races
Security Protocols and Specifications
FoSSaCS (1999), pp. 1-13
A Calculus for Cryptographic Protocols: The spi Calculus
Secure Communications Processing for Distributed Languages
Cédric Fournet
Georges Gonthier
IEEE Symposium on Security and Privacy (1999), pp. 74-88
Types for Safe Locking
A Type System for Java Bytecode Subroutines
Protection in Programming-Language Translations
Secure Internet Programming (1999), pp. 19-34
A Core Calculus of Dependency
A Top-Down Look at a Secure Message
Secure Network Objects
Leendert van Doorn
Michael Burrows
Edward Wobber
Secure Internet Programming (1999), pp. 395-412
Secrecy in Programming-Language Semantics
Electr. Notes Theor. Comput. Sci., vol. 20 (1999), pp. 80-94
A Bisimulation Method for Cryptographic Protocols
A Type System for Java Bytecode Subroutines
Panel Introduction: Varieties of Authentication
Roberto Gorrieri
Paul F. Syverson
Riccardo Focardi
Dieter Gollmann
Gavin Lowe
Catherine Meadows
CSFW (1998), pp. 79-82
On SDSI's Linked Local Name Spaces
Journal of Computer Security, vol. 6 (1998), pp. 3-22
Two Facets of Authentication
CSFW (1998), pp. 27-32
A Bisimulation Method for Cryptographic Protocols
Secure Web Tunneling
Andrew Birrell
Raymie Stata
Edward Wobber
Computer Networks, vol. 30 (1998), pp. 531-539
Protection in Programming-Language Translations
ICALP (1998), pp. 868-883
Secure Implementation of Channel Abstractions
Protection in Programming-Language Translations: Mobile Object Systems (Abstract)
ECOOP Workshops (1998), pp. 291
Secure Implementation of Channel Abstractions
Cédric Fournet
Georges Gonthier
Electr. Notes Theor. Comput. Sci., vol. 10 (1997), pp. 202-203
Explicit Communication Revisited: Two New Attacks on Authentication Protocols
IEEE Trans. Software Eng., vol. 23 (1997), pp. 185-186
A Calculus for Cryptographic Protocols: The Spi Calculus
Andrew D. Gordon
ACM Conference on Computer and Communications Security (1997), pp. 36-47
On SDSI's Linked Local Name Spaces
CSFW (1997), pp. 98-108
Secrecy by Typing inSecurity Protocols
TACS (1997), pp. 611-638
A Logic of Object-Oriented Programs
Reasoning about Cryptographic Protocols in the Spi Calculus
On Subtyping and Matching
Secure Network Objects
Leendert van Doorn
Michael Burrows
Edward Wobber
IEEE Symposium on Security and Privacy (1996), pp. 211-221
Analysis and Caching of Dependencies
On TLA as a logic
A Theory of Objects
Prudent Engineering Practice for Cryptographic Protocols
An Interpretation of Objects and Object Types
Syntactic Considerations on Recursive Types
A Theory of Primitive Objects: Untyped and First-Order Systems
Methods as Assertions
An Imperative Object Calculus (Invited Paper)
A Model for Formal Parametric Polymorphism: A PER Interpretation for System R
Dynamic Typing in Polymorphic Languages
Luca Cardelli
Benjamin C. Pierce
Didier Rémy
J. Funct. Program., vol. 5 (1995), pp. 111-130
A Theory of Primitive Objects: Second-Order Systems
An Abstract Account of Composition
Conjoining Specifications
An Imperative Object Calculus
On Subtyping and Matching
Authentication in the Taos Operating System
Prudent engineering practice for cryptographic protocols
Decidability and Expressiveness for First-Order Logics of Probability
A Semantics for Static Type Inference in a Nondeterministic Language
Inf. Comput., vol. 109 (1994), pp. 300-306
A Theory of Primitive Objects - Scond-Order Systems
An Old-Fashined Recipe for Real-Time
Decomposing Specifications of Concurrent Systems
Baby Modula-3 and a Theory of Objects
J. Funct. Program., vol. 4 (1994), pp. 249-283
A Theory of Primitive Objects - Untyped and First-Order Systems
Methods as Assertions
Open Systems in TLA
A TLA Solution to the RPC-Memory Specification Problem
Subtyping and Parametricity
A Semantics of Object Types
Authentification and Delegation with Smart-Cards
Michael Burrows
C. Kaufman
Butler W. Lampson
Sci. Comput. Program., vol. 21 (1993), pp. 93-113
A Logic for Parametric Polymorphism
Extensible Grammars for Language Specialization
Formal Parametric Polymorphism
Authentication in the Taos Operating System
Composing Specifications
A Logical View of Composition
Formal Parametric Polymorphism
A Calculus for Access Control in Distributed Systems
Michael Burrows
Butler W. Lampson
Gordon D. Plotkin
ACM Trans. Program. Lang. Syst., vol. 15 (1993), pp. 706-734
Authentication in Distributed Systems: Theory and Practice
Butler W. Lampson
Michael Burrows
Edward Wobber
ACM Trans. Comput. Syst., vol. 10 (1992), pp. 265-310
Linear Logic Without Boxes
The Geometry of Optimal Lambda Reduction
Faithful Ideal Models for Recursive Polymorphic Types
Benjamin C. Pierce
Gordon D. Plotkin
Int. J. Found. Comput. Sci., vol. 2 (1991), pp. 1-21
Explicit Substitutions
Luca Cardelli
Pierre-Louis Curien
Jean-Jacques Lévy
J. Funct. Program., vol. 1 (1991), pp. 375-416
Preserving Liveness: Comments on ``Safety and Liveness from a Methodological Point of View''
Bowen Alpern
Krzysztof R. Apt
Nissim Francez
Shmuel Katz
Leslie Lamport
Fred B. Schneider
Inf. Process. Lett., vol. 40 (1991), pp. 141-142
The Existence of Refinement Mappings
A Semantics for a Logic of Authentication (Extended Abstract)
An Old-Fashioned Recipe for Real Time
A Calculus for Access Control in Distributed Systems
A Logical View of Composition and Refinement
Authentication in Distributed Systems: Theory and Practice
Authentication and Delegation with Smart-cards
Dynamic Typing in a Statically Typed Language
Luca Cardelli
Benjamin C. Pierce
Gordon D. Plotkin
ACM Trans. Program. Lang. Syst., vol. 13 (1991), pp. 237-268
A Logic of Authentication
Corrigendum: The Power of Temporal Proofs
Theor. Comput. Sci., vol. 70 (1990), pp. 275
Explicit Substitutions
Nonclausal Deduction in First-Order Temporal Logic
A Per Model of Polymorphism and Recursive Types
Rejoinder to Nessett
Secure Circuit Evaluation
An Axiomatization of Lamport's Temporal Logic of Actions
CONCUR (1990), pp. 57-69
Realizable and Unrealizable Specifications of Reactive Systems
Dynamic Typing in a Statically-Typed Language
A Logic of Authentication
Decidability and Expressiveness for First-Order Logics of Probability (Extended Abstract)
Faithful Ideal Models for Recursive Polymorphic Types
On Hiding Information from an Oracle
Temporal Logic Programming
Composing Specifications
The Power of Temporal Proofs
Theor. Comput. Sci., vol. 65 (1989), pp. 35-83
On Generating Solved Instances of Computational Problems
Eric Allender
Joan Feigenbaum
Lane A. Hemachandra
CRYPTO (1988), pp. 297-310
Authentication: A Practical Study in Belief and Action
The Existence of Refinement Mappings
A Simple Protocol for Secure Circuit Evaluation
On hiding information from an oracle
The Power of Temporal Proofs
LICS (1987), pp. 123-130
Temporal Logic Programming
On Hiding Information from an Oracle (Extended Abstract)
A Timely Resolution
Modal Theorem Proving
Nonclausal Temporal Deduction
