74 citations · 173 across the 9 of their papers we have counts for
9 papers
Mathematical Proof Between Generations
Jonas Bayer, Christoph Benzmüller, Kevin Buzzard +7
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This…
The TLA+ Toolbox
Markus Alexander Kuppe, Leslie Lamport, Daniel Ricketts
We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineer…
On the Glitch Phenomenon
Leslie Lamport, Richard Palais
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 arb…
Auxiliary Variables in TLA+
Leslie Lamport, Stephan Merz
Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implem…
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Damien Doligez, Jael Kriener, Leslie Lamport +2
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.
TLA+ Proofs
Denis Cousineau, Damien Doligez, Leslie Lamport +3
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 wi…