74 citations · 92 across the 6 of their papers we have counts for
6 papers
Proceedings ML Family / OCaml Users and Developers workshops
Jeremy Yallop, Damien Doligez
This volume contains the joint post-proceedings of the 2015 edition of the ML Family Workshop and OCaml Users and Developers Workshop, held in Vancouver, British Columbia, Canada,…
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.
Experience in using a typed functional language for the development of a security application
Damien Doligez, Christèle Faure, Thérèse Hardin +1
In this paper we present our experience in developing a security application using a typed functional language. We describe how the formal grounding of its semantic and compiler ha…
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…
Verifying Safety Properties With the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport +1
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 element…
A TLA+ Proof System
Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport +1
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 l…