# Leslie Lamport - MSR - INRIA

## Contact Details

NameLeslie Lamport |
||

AffiliationMSR - INRIA |
||

Location |
||

## Pubs By Year |
||

## Pub CategoriesComputer Science - Logic in Computer Science (5) Computer Science - Software Engineering (1) Computer Science - Databases (1) Computer Science - Distributed; Parallel; and Cluster Computing (1) Mathematics - Optimization and Control (1) Mathematics - Dynamical Systems (1) Mathematics - Information Theory (1) Computer Science - Information Theory (1) |

## Publications Authored By Leslie Lamport

The Principle of the Glitch states that for any device which makes a discrete decision based upon a continuous range of possible inputs, there are inputs for which it will take arbitrarily long to reach a decision. The appropriate mathematical setting for studying this principle is described. This involves defining the concept of continuity for mappings on sets of functions. Read More

**Affiliations:**

^{1}VERIDIS,

^{2}VERIDIS

With state-based methods, checking that an implementation satisfies a higher-level specification requires describing how the higher-level concepts in the specification are represented by the lower-level data structures of the implementation. This approach was first proposed in the domain of sequential systems by Hoare in 1972. Hoare called the description an abstraction function. Read More

**Authors:**Damien Doligez

^{1}, Jael Kriener

^{2}, Leslie Lamport

^{3}, Tomer Libal

^{4}, Stephan Merz

^{5}

**Affiliations:**

^{1}INRIA Paris-Rocquencourt,

^{2}MSR - INRIA,

^{3}MSR - INRIA,

^{4}MSR - INRIA,

^{5}INRIA Nancy - Grand Est / LORIA

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic. Read More

TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs. Read More

**Affiliations:**

^{1}INRIA Saclay - Ile de France,

^{2}INRIA Rocquencourt,

^{3}INRIA Lorraine,

^{4}INRIA Lorraine

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. Read More

**Affiliations:**

^{1}MRI,

^{2}INRIA Rocquencourt,

^{3}INRIA Lorraine - LORIA,

^{4}INRIA Lorraine - LORIA

We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Read More

The distributed transaction commit problem requires reaching agreement on whether a transaction is committed or aborted. The classic Two-Phase Commit protocol blocks if the coordinator fails. Fault-tolerant consensus algorithms also reach agreement, but do not block whenever any majority of the processes are working. Read More