5 citations · 13 across the 5 of their papers we have counts for
Showing 2012Show all
2 papers · 1 filter
cs.SE2012
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…
cs.LO2012★ 4 cited
On completeness of reducibility candidates as a semantics of strong normalization
Denis Cousineau
This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo à la Curry.…