Paper Info
Title
Type Checking Circus Specifications
Abstract
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.
Year
DOI
Venue
2008
10.1016/j.entcs.2007.08.027
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
circus type system,formal languages,additional constructor,type checker,robust construction,typing rule,formal methods,circus tool,formal language,state-rich reactive system,refinement calculus,concurrency,refinement tool,type checking circus specifications,type system,formal method,reactive system
Programming language,Formal language,Type checking,Refinement calculus,Computer science,Concurrency,Theoretical computer science,Formal methods,Reactive system
Journal
Volume
ISSN
Citations 
195,
Electronic Notes in Theoretical Computer Science
7
PageRank 
References 
Authors
0.58
10
3
Name
Order
Citations
PageRank
Manuela Xavier1191.87
Ana Cavalcanti266859.95
Augusto Sampaio350143.38