| 摘要 |
A type annotation technique such that expressions are assigned and annotated with types in such a way that types can be efficiently maintained during inference without new syntactic restrictions being placed on the expressions or underlying logic within the verification system. More particularly, in accordance with the technique, expressions, i.e. terms, are annotated using a particular labeling scheme such that, during verification, if an expression is annotated the verification may proceed without any additional type inference or type checking with regard to that expression.
|
