Paper Info
Title
Static typing with value space-based subtyping
Abstract
Numerous programming and schema languages contain the notion of value types. However, support for value space-based subtyping is spotty. This paper presents a formal type system for atomic value types as an extension of the simply typed lambda calculus with subtyping. In the λc-calculus, value types can be derived through the application of value space constraints. Type inference rules can be used to infer transient value space constraints that hold for limited scopes of a program. The type system of the λc-calculus is proved to be sound. The λc-calculus was fully implemented in Java and C#. The presented approach was successfully validated to subsume XML Schema Definition type construction and to facilitate the integration of XSD data types with the C# programming language.
Year
DOI
Venue
2011
10.1145/2072221.2072242
SAICSIT Conf.
Keywords
Field
DocType
type inference rule,value space constraint,value space-based subtyping,transient value space constraint,xsd data type,xml schema definition type,formal type system,atomic value type,static typing,type system,value type,value types,typed lambda calculus,type inference,xml schema,data type
Covariance and contravariance,Type system,Programming language,Typed lambda calculus,Computer science,Composite data type,Type inference,Generalized algebraic data type,Dependent type,Type constructor
Conference
Citations 
PageRank 
References 
0
0.34
9
Authors
2
Name
Order
Citations
PageRank
Alexander Paar1446.69
Stefan Gruner2185.57