A Causal Logic of Events in Formalized Computational Type Theory
Mark Bickford, Robert L. Constable · eCommons (Cornell University) · 2005
We provide a logic for distributed computing that has the explanatory and technical power of constructive logics of computation. Inparticular, 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.