Coinductive Type Systems for Object-Oriented Languages
Coinductive Type Systems for Object-Oriented Languages
复制标题
面向对象语言的共归纳类型系统
DOI：
10.1007/978-3-642-03013-0_2
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Giovanni Lagorio
中科院分区：
文献类型：
--
作者：
D. Ancona;Giovanni Lagorio
提出了一种基于共归纳逻辑的编程语言类型系统指定方法。
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.