3 citations · 3 across the 1 of their papers we have counts for
3 papers
cs.LO2018★ 3 cited
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl
Mark Bickford
This article is the first in a series of articles that explain the formalization of a constructive model of cubical type theory in Nuprl. In this document we discuss only the parts…
cs.LO2011
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…
cs.LO2009
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…