Model verification in λσ: a type inference approach

The author describes a number of model analysis and verification operations based on type inference in the λσ simulation language. λσ is a simulation language based on the typed λ-calculus. λσ entities correspond to typed λ-expressions, while λσ activities correspond to subtypes. Thus, entities can be generated by means of type-introduction rules, and operations can be defined on entities by means of type elimination and equality rules. Premises of the form e∈τ in an introduction rule used to create a new entity can be satisfied by substituting for e any entity of type τ in a neighboring activity. It is then possible to perform a number of model analysis and verification operations using type inference algorithms available for the typed λ-calculus