A Causal Logic of Events in Formalized Computational Type Theory

Book Article Version [PDF]

Tech Report Version
unofficial copies [PDF], [PS]

by Mark Bickford and Robert L. Constable

Cornell University Technical Report 2005-2010, 2005.


We provide a logic for distributed computing that has the explanatory and technical
power of constructive logics of computation. In particular, we establish a proof technology
that supports correct-by-construction programming based on the notion that
concurrent processes can be extracted from proofs that specifications are achievable.