Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas

In recent work we have shown how it is possible to define very precise type systems for object-oriented languages by abstractly compiling a program into a Horn formula f. Then type inference amounts to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of f. Type...

Full description

Bibliographic Details
Main Authors: Davide Ancona, Giovanni Lagorio
Format: Article
Language:English
Published: Open Publishing Association 2010-06-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1006.1413v1