215 citations
- Microsoft (United States)US11 papers
- University of CambridgeGB5 papers
- Johns Hopkins UniversityUS4 papers
- Massachusetts Institute of TechnologyUS4 papers
- Tel Aviv UniversityIL4 papers
- University of California, BerkeleyUS4 papers
- University of ChicagoUS4 papers
- Microsoft Research New England (United States)US3 papers
- Stanford UniversityUS3 papers
- University of British ColumbiaCA3 papers
- University of MichiganUS3 papers
- University of PennsylvaniaUS3 papers
Showing 2008 · cs.LOShow all
3 papers · 2 filters
cs.LO2008★ 17 cited
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…
cs.LO2008★ 7 cited
Two Forms of One Useful Logic: Existential Fixed Point Logic and Liberal Datalog
Andreas Blass, Yuri Gurevich
A natural liberalization of Datalog is used in the Distributed Knowledge Authorization Language (DKAL). We show that the expressive power of this liberal Datalog is that of existen…
cs.LO2008
One useful logic that defines its own truth
Andreas Blass, Yuri Gurevich
Existential fixed point logic (EFPL) is a natural fit for some applications, and the purpose of this talk is to attract attention to EFPL. The logic is also interesting in its own…