Search: id:"swepub:oai:research.chalmers.se:677c1794-46e3-4185-a487-56fd37a0d579" >
Coercive subtyping ...
Abstract
Subject headings
Close
- We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF< .
Subject headings
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Type theory
- Metatheory
- Typecasting
- Coercive subtyping
- Lambda-free logical framework
Publication and Content Type
- kon (subject category)
- ref (subject category)
To the university's database