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
Nicolas Papernot
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
Geoffrey Irving
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
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, 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
Geoffrey Irving
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
Timely Rollback: Specification and Verification
Foundations of Differential Dataflow
On the Flow of Data, Information, and Time
The Prophecy of Undo
FASE(2015), pp. 347-361
Understanding Typescript
Gavin M. Bierman
Mads Torgersen
ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, pp. 257-281
Web PKI: Closing the Gap between Guidelines and Practices
Antoine Delignat-Lavaud
Andrew Birrell
Ilya Mironov
Ted Wobber
Yinglian Xie
Microsoft Research
NDSS(2014)
Formal Analysis of a Distributed Algorithm for Tracking Progress
Early security classification of skype users via machine learning
Message-Locked Encryption for Lock-Dependent Messages
Global Authentication in an Untrustworthy World
Layout Randomization and Nondeterminism
Jérémy Planul
Gordon D. Plotkin
Electr. Notes Theor. Comput. Sci., 298(2013), pp. 29-50
On Layout Randomization for Arrays and Functions
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
Naiad: a timely dataflow system
Frank McSherry
Rebecca Isaacs
SOSP(2013), pp. 439-455
Host Fingerprinting and Tracking on the Web: Privacy and Security Implications
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
Software Security: A Formal Perspective - (Notes for a Talk)
FM(2012), pp. 1-5
A Functional View of Imperative Information Flow
On Protection by Layout Randomization
Heat-seeking honeypots: design and experience
Differential privacy with information flow control
Semantics of transactional memory and automatic mutual exclusion
Andrew Birrell
Tim Harris 0001
ACM Trans. Program. Lang. Syst., 33(2011), pp. 2
AC: composable asynchronous IO for native languages
deSEO: Combating Search-Result Poisoning
A Model of Cooperative Threads
On Protection by Layout Randomization
A model of dynamic separation for transactional memory
Guessing attacks and the computational soundness of static equivalence
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
Searching the Searchers with SearchAudit
John P. John
Fang Yu
Yinglian Xie
Arvind Krishnamurthy
USENIX Security Symposium(2010), pp. 127-142
The Fine Print of Security
LICS(2010), pp. 110
Transactional memory with strong atomicity using off-the-shelf memory protection hardware
Unified Declarative Platform for Secure Netwoked Information Systems
Perspectives on Transactional Memory
Models and Proofs of Protocol Security: A Progress Report
De-anonymizing the internet using unreliable IDs
Implementation and Use of Transactional Memory with Dynamic Separation
A model of cooperative threads
Logic in Access Control (Tutorial Notes)
FOSAD(2009), pp. 145-165
Control-flow integrity principles, implementations, and applications
Variations in Access Control Logic
DEON(2008), pp. 96-109
Automated verification of selected equivalences for security protocols
Automatic Mutual Exclusion and Atomicity Checks
Concurrency, Graphs and Models(2008), pp. 510-526
A Model of Dynamic Separation for Transactional Memory
The good, the bad, and the provable
ACM Conference on Computer and Communications Security(2008), pp. 1
Semantics of transactional memory and automatic mutual exclusion
Code-Carrying Authorization
Security analysis of cryptographically controlled access to XML documents
A Modal Deconstruction of Access Control Logics
Authorizing applications in singularity
Ted Wobber
Aydan R. Yumerefendi
Andrew Birrell
Daniel R. Simon
EuroSys(2007), pp. 355-368
Just fast keying in the pi calculus
Security Protocols: Principles and Calculi
FOSAD(2007), pp. 1-23
Policies and Proofs for Code Auditing
Editorial
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Access Control in a Core Calculus of Dependency
Electr. Notes Theor. Comput. Sci., 172(2007), pp. 5-31
Towards a Declarative Language and System for Secure Networking
Types for safe locking: Static race detection for Java
Cormac Flanagan
Stephen N. Freund
ACM Trans. Program. Lang. Syst., 28(2006), pp. 207-255
Architectural support for software-based protection
Access control in a core calculus of dependency
ICFP(2006), pp. 263-273
XFI: Software Guards for System Address Spaces
Guessing Attacks and the Computational Soundness of Static Equivalence
Computational Secrecy by Typing for the Pi Calculus
Formal Analysis of Dynamic, Distributed File-System Access Controls
Deciding knowledge in security protocols under equational theories
Secrecy by Typing and File-Access Control
Computer-assisted verification of a protocol for certified email
Deciding Knowledge in Security Protocols under (Many More) Equational Theories
Moderately hard, memory-bound functions
Michael M. Burrows
Mark Manasse
Ted Wobber
ACM Transactions on Internet Technology, 5(2005), pp. 299-327
Analyzing security protocols with secrecy types and logic programs
A Theory of Secure Control Flow
Password-Based Encryption Analyzed
"Language-Based Security"
Formal security analysis of basic network-attached storage
Control-flow integrity
Mihai Budiu
Úlfar Erlingsson
Jay Ligatti
ACM Conference on Computer and Communications Security(2005), pp. 340-353
Automated Verification of Selected Equivalences for Security Protocols
Security analysis of cryptographically controlled access to XML documents
Access Control in a World of Software Diversity
Private authentication
Just Fast Keying in the Pi Calculus
BCiC: A System for Code Authentication and Verification
Deciding Knowledge in Security Protocols Under Equational Theories
By Reason and Authority: A System for Authorization of Proof-Carrying Code
Language-Based Enforcement of Privacy Policies
A Logical Account of NGSCB
Trusted Computing, Trusted Third Parties, and Verified Communications
SEC(2004), pp. 291-308
Choice in Dynamic Linking
Reasoning About Secrecy for Active Networks
Secrecy types for asymmetric communication
Bankable Postage for Network Services
Access Control Based on Execution History
Computer-Assisted Verification of a Protocol for Certified Email
Built-in Object Security
ECOOP(2003), pp. 1
Logic in Access Control
LICS(2003), pp. 228-
A Logic of Object-Oriented Programs
Hiding Names: Private Authentication in the Applied Pi Calculus
Private Authentication
Privacy Enhancing Technologies(2002), pp. 27-40
Secure Implementation of Channel Abstractions
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Editorial
Analyzing security protocols with secrecy types and logic programs
Certified email with a light on-line trusted third party: design and implementation
Computing Symbolic Models for Verifying Cryptographic Protocols
Formal Eavesdropping and Its Computational Interpretation
Leslie Lamport's properties and actions
PODC(2001), pp. 15
Mobile values, new names, and secure communication
Secrecy Types for Asymmetric Communication
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Authentication Primitives and Their Compilation
top-top-closed relations and admissibility
Mathematical Structures in Computer Science, 10(2000), pp. 313-320
Reasoning about Secrecy for Active Networks
Taming the Adversary
CRYPTO(2000), pp. 353-358
A Core Calculus of Dependency
Secure Network Objects
Leendert van Doorn
Michael Burrows
Edward Wobber
Secure Internet Programming(1999), pp. 395-412
Security Protocols and Specifications
FoSSaCS(1999), pp. 1-13
Protection in Programming-Language Translations
Secure Internet Programming(1999), pp. 19-34
A Top-Down Look at a Secure Message
Secure Communications Processing for Distributed Languages
Cédric Fournet
Georges Gonthier
IEEE Symposium on Security and Privacy(1999), pp. 74-88
A Calculus for Cryptographic Protocols: The spi Calculus
Types for Safe Locking
Secrecy in Programming-Language Semantics
Electr. Notes Theor. Comput. Sci., 20(1999), pp. 80-94
A Type System for Java Bytecode Subroutines
Object Types against Races
Secure Web Tunneling
Secure Implementation of Channel Abstractions
Panel Introduction: Varieties of Authentication
Roberto Gorrieri
Paul F. Syverson
Riccardo Focardi
Dieter Gollmann
Gavin Lowe
Catherine Meadows
CSFW(1998), pp. 79-82
A Bisimulation Method for Cryptographic Protocols
A Type System for Java Bytecode Subroutines
Protection in Programming-Language Translations
ICALP(1998), pp. 868-883
A Bisimulation Method for Cryptographic Protocols
Protection in Programming-Language Translations: Mobile Object Systems (Abstract)
ECOOP Workshops(1998), pp. 291
On SDSI's Linked Local Name Spaces
Journal of Computer Security, 6(1998), pp. 3-22
Two Facets of Authentication
CSFW(1998), pp. 27-32
Explicit Communication Revisited: Two New Attacks on Authentication Protocols
IEEE Trans. Software Eng., 23(1997), pp. 185-186
Secure Implementation of Channel Abstractions
Cédric Fournet
Georges Gonthier
Electr. Notes Theor. Comput. Sci., 10(1997), pp. 202-203
On SDSI's Linked Local Name Spaces
CSFW(1997), pp. 98-108
A Logic of Object-Oriented Programs
Reasoning about Cryptographic Protocols in the Spi Calculus
A Calculus for Cryptographic Protocols: The Spi Calculus
Andrew D. Gordon
ACM Conference on Computer and Communications Security(1997), pp. 36-47
Secrecy by Typing inSecurity Protocols
TACS(1997), pp. 611-638
Syntactic Considerations on Recursive Types
On Subtyping and Matching
A Theory of Primitive Objects: Untyped and First-Order Systems
A Theory of Objects
Analysis and Caching of Dependencies
On TLA as a logic
An Interpretation of Objects and Object Types
Secure Network Objects
Leendert van Doorn
Michael Burrows
Edward Wobber
IEEE Symposium on Security and Privacy(1996), pp. 211-221
Prudent Engineering Practice for Cryptographic Protocols
Dynamic Typing in Polymorphic Languages
On Subtyping and Matching
A Model for Formal Parametric Polymorphism: A PER Interpretation for System R
An Imperative Object Calculus
A Theory of Primitive Objects: Second-Order Systems
Methods as Assertions
An Abstract Account of Composition
An Imperative Object Calculus (Invited Paper)
Conjoining Specifications
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., 109(1994), pp. 300-306
Baby Modula-3 and a Theory of Objects
J. Funct. Program., 4(1994), pp. 249-283
A Theory of Primitive Objects - Scond-Order Systems
A Theory of Primitive Objects - Untyped and First-Order Systems
An Old-Fashined Recipe for Real-Time
Authentication in the Taos Operating System
A Semantics of Object Types
A TLA Solution to the RPC-Memory Specification Problem
Decomposing Specifications of Concurrent Systems
Subtyping and Parametricity
Open Systems in TLA
Methods as Assertions
Formal Parametric Polymorphism
A Logic for Parametric Polymorphism
A Logical View of Composition
Extensible Grammars for Language Specialization
A Calculus for Access Control in Distributed Systems
Michael Burrows
Butler W. Lampson
Gordon D. Plotkin
ACM Trans. Program. Lang. Syst., 15(1993), pp. 706-734
Authentification and Delegation with Smart-Cards
Michael Burrows
C. Kaufman
Butler W. Lampson
Sci. Comput. Program., 21(1993), pp. 93-113
Composing Specifications
Formal Parametric Polymorphism
Authentication in the Taos Operating System
Linear Logic Without Boxes
Authentication in Distributed Systems: Theory and Practice
Butler W. Lampson
Michael Burrows
Edward Wobber
ACM Trans. Comput. Syst., 10(1992), pp. 265-310
The Geometry of Optimal Lambda Reduction
Faithful Ideal Models for Recursive Polymorphic Types
Authentication and Delegation with Smart-cards
Authentication in Distributed Systems: Theory and Practice
Dynamic Typing in a Statically Typed Language
Luca Cardelli
Benjamin C. Pierce
Gordon D. Plotkin
ACM Trans. Program. Lang. Syst., 13(1991), pp. 237-268
The Existence of Refinement Mappings
A Calculus for Access Control in Distributed Systems
An Old-Fashioned Recipe for Real Time
A Logical View of Composition and Refinement
A Semantics for a Logic of Authentication (Extended Abstract)
Explicit Substitutions
Luca Cardelli
Pierre-Louis Curien
Jean-Jacques Lévy
J. Funct. Program., 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., 40(1991), pp. 141-142
Explicit Substitutions
A Logic of Authentication
Nonclausal Deduction in First-Order Temporal Logic
A Per Model of Polymorphism and Recursive Types
Secure Circuit Evaluation
An Axiomatization of Lamport's Temporal Logic of Actions
CONCUR(1990), pp. 57-69
Corrigendum: The Power of Temporal Proofs
Theor. Comput. Sci., 70(1990), pp. 275
Rejoinder to Nessett
Composing Specifications
Faithful Ideal Models for Recursive Polymorphic Types
A Logic of Authentication
On Hiding Information from an Oracle
Decidability and Expressiveness for First-Order Logics of Probability (Extended Abstract)
Temporal Logic Programming
Realizable and Unrealizable Specifications of Reactive Systems
The Power of Temporal Proofs
Theor. Comput. Sci., 65(1989), pp. 35-83
Dynamic Typing in a Statically-Typed Language
Authentication: A Practical Study in Belief and Action
The Existence of Refinement Mappings
A Simple Protocol for Secure Circuit Evaluation
On Generating Solved Instances of Computational Problems
Eric Allender
Joan Feigenbaum
Lane A. Hemachandra
CRYPTO(1988), pp. 297-310
On Hiding Information from an Oracle (Extended Abstract)
Temporal Logic Programming
On hiding information from an oracle
The Power of Temporal Proofs
LICS(1987), pp. 123-130
Modal Theorem Proving
A Timely Resolution
Nonclausal Temporal Deduction