Module Compiler implements the functions needed for compiling Quartz modules to AIF modules, as well as functions for linking AIF modules to AIF systems.

Module Statements implements the data type for typed statements that are obtained from the type-checker implemented in module UtyStmts and are given to the compile functions.

Module UtyExprs implements data types for untyped expressions that are used to store parse trees of program expressions and specifications. Given a declaration of the used variables, the module provides also functions to convert these untyped constructs to corresponding typed constructs according to the type rules of the Quartz language.

Module UtyStmts implements data types for untyped statements that are used to store parse trees of Quartz statements and modules. The module provides also functions to convert these untyped constructs to corresponding typed statements and modules according to the type rules of the Quartz language.