A Causal Logic of Events in Formalized Computational Type Theory

Book Article Version [PDF]

Tech Report Version
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-2010
unofficial copies [PDF], [PS]

by Mark Bickford and Robert L. Constable

Cornell University Technical Report 2005-2010, 2005.

Abstract

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.