A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics
Random Access Machines (RAMs) are a deterministic Turing-complete formalism especially well suited for being encoded in other formalisms. This is due to the fact that RAMs can be defined starting from very primitive concepts and operations, which are unbounded natural numbers, tuples, successor, predecessor and test for equality to zero. Since these concepts are easily available also in theorem-provers and proof-assistants, RAMs are good candidates for proving Turing-completeness of formalisms using a proof-assistant. In this paper we describe an encoding in Coq of RAMs into a Linda Calculus endowed with the Ordered Semantics. We discuss the main difficulties that must be faced and the techniques we adopted to solve them.
KeywordsParallel Composition Process Algebra Constructive Proof Program Counter Tuple Space
Unable to display preview. Download preview PDF.
- 2.The Coq proof-assistant, http://coq.inria.fr/
- 3.Hofmann, M.: Extensional concepts in intensional type theory. Ph.D. thesis, University of Edinburgh (July 1995)Google Scholar
- 4.McBride, C.: Dependently Typed Functional Programs and their Proofs. Ph.D. thesis, University of Edinburgh (2000)Google Scholar
- 8.Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical Knowledge Management in HELM. In: On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM 2001), RISCLinz, Austria (September 2001)Google Scholar
- 9.Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: XML, Stylesheets and the re-mathematization of Formal Content. In: On-Line Proceedings of EXTREME 2001 (2001)Google Scholar
- 10.Milner, R.: The Polyadic π-Calculus: A Tutorial Technical Report, Department of Computer Science, University of Edinburgh, ECS-LFCS-91-180 (October 1991)Google Scholar