Verifying Process Algebra Proofs in Type Theory
Publication date
1993-03
Authors
Sellink, M.P.A.
Editors
Advisors
Supervisors
DOI
Document Type
Preprint
Metadata
Show full item recordCollections
License
Abstract
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.