Advertisement
Published in:
2009 | OriginalPaper | Chapter
Coinductive Type Systems for Object-Oriented Languages
Authors : Davide Ancona, Giovanni Lagorio
Published in: ECOOP 2009 – Object-Oriented Programming
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We propose a novel approach based on coinductive logic to specify type systems of programming languages.
The approach consists in encoding programs in Horn formulas which are interpreted w.r.t. their coinductive Herbrand model.
We illustrate the approach by first specifying a standard type system for a small object-oriented language similar to Featherweight Java. Then we define an idealized type system for a variant of the language where type annotations can be omitted. The type system involves infinite terms and proof trees not representable in a finite way, thus providing a theoretical limit to type inference of object-oriented programs, since only sound approximations of the system can be implemented.
Approximation is naturally captured by the notions of subtyping and subsumption; indeed, rather than increasing the expressive power of the system, as it usually happens, here subtyping is needed for approximating infinite non regular types and proof trees with regular ones.