<XML><RECORDS><RECORD><REFERENCE_TYPE>10</REFERENCE_TYPE><REFNUM>9276</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR></AUTHORS><YEAR>2006</YEAR><TITLE>Subtyping between Standard and Linear Function Types</TITLE><PLACE_PUBLISHED>DCS Technical Report Series</PLACE_PUBLISHED><PUBLISHER>Dept of Computing Science, University of Glasgow</PUBLISHER><ISBN>TR-2006-305</ISBN><LABEL>Gay:2006:9276</LABEL><KEYWORDS><KEYWORD>functional programming</KEYWORD></KEYWORDS<ABSTRACT>As an abstraction of functional programming languages in which certain runtime entities are required to be uniquely referenced, we define a lambda-calculus with both linear and standard data types and consequently both linear and standard function types. We use a single syntax for both linear and standard functions, and rely on the typechecker to produce a linear function type only when necessary. To compensate for the typechecker's preference for standard function types, we include a subtyping relation in which the standard function type is a subtype of the linear function type. We prove that typing guarantees unique references to values of linear data types, that typing is preserved by the operational semantics, and that the typechecking algorithm is sound and complete with respect to the declarative typing rules.</ABSTRACT></RECORD></RECORDS></XML>