Verifying Process Algebra Proofs in Type Theory
M.P.A. Sellink · Utrecht University Repository (Utrecht University) · 1993
In this paper we study automatic verification of proofs in process algebra. Formulas of process algebra are represented by types in typed λ-calculus. Inhabitants (terms) of these types represent proofs. The specific typed λ-calculus we use is the Calculus of Inductive Constructions as implemented in the interactive proof construction program COQ.