1 citations · 1 across the 1 of their papers we have counts for
5 papers
Virtual Evidence: A Constructive Semantics for Classical Logics
Robert L. Constable
This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Exclud…
Intuitionistic Completeness of First-Order Logic
Robert Constable, Mark Bickford
We establish completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable if and only if its embedding into minimal logic, mFOL, is uniformly valid u…
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP
Robert Constable
The Fischer-Lynch-Paterson theorem (FLP) says that it is impossible for processes in an asynchronous distributed system to achieve consensus on a binary value when a single process…
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
Mark Bickford, Robert Constable, Joseph Halpern +1
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. Thi…
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics
Robert Constable, Wojciech Moczydlowski
Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. W…