Sciweavers

Share
TABLEAUX
2005
Springer

A Calculus for Type Predicates and Type Coercion

10 years 18 days ago
A Calculus for Type Predicates and Type Coercion
We extend classical first-order logic with subtyping by type predicates and type coercion. Type predicates assert that the value of a term belongs to a more special type than the signature guarantees, while type coercion allows using terms of a more general type where the signature calls for a more special one. These operations are important e.g. in the specification and verification of object-oriented programs. We present a tableau calculus for this logic and prove its completeness.
Martin Giese
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TABLEAUX
Authors Martin Giese
Comments (0)
books