Type Checking Circus Specifications

Citations of this article
Mendeley users who have this article in their library.


Circus is a formal language that combines Z, CSP and additional constructors of Morgan's refinement calculus. It is aimed at the development by refinement of state-rich reactive systems. In this work, we define the Circus type system and describe the design and implementation of a type checker. We developed the type checker based directly on the typing rules that formalise the type system of Circus. We believe that this contributed to the robust construction of the type checker. We also discuss the validation strategy of the type checker, including integrations with other Circus tools. © 2008 Elsevier B.V. All rights reserved.




Xavier, M., Cavalcanti, A., & Sampaio, A. (2008). Type Checking Circus Specifications. Electronic Notes in Theoretical Computer Science, 195(C), 75–93. https://doi.org/10.1016/j.entcs.2007.08.027

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free