Type checking mCRL2

    Research output: Book/ReportReportAcademic

    82 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


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

    Cite this