Verifying Process Algebra Proofs in Type Theory

In this paper we study automatic veri cation of proofs in process algebra. Formulas of process algebra are represented by types in typed -calculus. Inhabitants (terms) of these types represent proofs. The speci c typed -calculus we use is the Calculus of Inductive Constructions as implemented in the interactive proof construction program COQ.

• Type: Conference
• Year: 1993
• Where: SOSL
• Authors: M. P. A. Sellink
• Keywords: Automatic Veri Cation, Natural Language Processing, Process Algebra, SOSL 1993, Types Represent Proofs