Skip to main content
PRL Project

A Causal Logic of Events in Formalized Computational Type Theory

by Mark Bickford, Robert L. Constable

  • Presented at Logical Aspects of Secure Computer Systems, Proceedings of International Summer School Marktoberdorf
  • unofficial PDF
  • 2005 - Cornell University Technical Report

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.

bibTex ref: BC05

cite link