Type checking mCRL2

Research output: Book/ReportReportAcademic

43 Downloads (Pure)


In this paper we present a type system for the data language of mCRL2, a process algebra based language for formalising the behaviour of communicating system. Much of the type system is standard, and follows the line of, e.g., Pierce [Pie02]. The data language that is described is rich, and supports (infinite) sets and bags, universal and existential quantification, and lambda abstraction. Recursive types can be defined using equational definitions. Subtyping is included for the full data language, and a coercion is given to transform a well-typed expression into a strictly typed expression.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages21
Publication statusPublished - 2011

Publication series

NameComputer science reports
ISSN (Print)0926-4515

Fingerprint Dive into the research topics of 'Type checking mCRL2'. Together they form a unique fingerprint.

  • Cite this

    Keiren, J. J. A., & Reniers, M. A. (2011). Type checking mCRL2. (Computer science reports; Vol. 1111). Eindhoven: Technische Universiteit Eindhoven.