A Calculus for Type Predicates and Type Coercion | Zendy

Martin Giese | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Calculus for Type Predicates and Type Coercion

Author(s) -

Martin Giese

Publication year - 2005

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-28931-3

DOI - 10.1007/11554554_11

Subject(s) - subtyping , signature (topology) , coercion (linguistics) , type (biology) , completeness (order theory) , computer science , programming language , calculus (dental) , automated theorem proving , first order logic , type theory , dependent type , theoretical computer science , lambda calculus , mathematics , linguistics , medicine , ecology , mathematical analysis , philosophy , geometry , dentistry , biology

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research