A Causal Logic of Events in Formalized Computational Type Theory
MetadataShow full item record
Bickford, Mark; Constable, Robert L.
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.
computer science; technical report
Previously Published As