Publications-Periodical Articles

Article View/Open

Publication Export

Google ScholarTM

NCCU Library

Citation Infomation

Related Publications in TAIR

題名 A Type System for a Lambda Calculus with Assignments
作者 Chen, Kung;Odersky, Martin
陳恭
貢獻者 資科系
日期 1994
上傳時間 17-Jun-2015 15:07:29 (UTC+8)
摘要 We present a Hindley/Milner-style polymorphic type system for var, an extension of the call-by-name -calculus with mutable variables and assignments. To match var`s explicit distinction between functional and imperative worlds, the type universe is stratified into two layers: one for applicative expressions and one for imperative state transformers. In inferring types for var-terms, the type system performs a simple effect analysis to statically verify the safety of coercing a state transformer to a pure value. We prove the soundness of the type system with respect to var`s untyped reduction semantics so that any well-typed program will evaluate to an answer, provided the evaluation terminates. We also discuss some practical aspects of the type system and present a type checker based on the well-known W algorithm.
關聯 Theoretical Aspects of Computer Software - TACS , pp. 347-364
資料類型 article
DOI http://dx.doi.org/10.1007/3-540-57887-0_103
dc.contributor 資科系
dc.creator (作者) Chen, Kung;Odersky, Martin
dc.creator (作者) 陳恭zh_TW
dc.date (日期) 1994
dc.date.accessioned 17-Jun-2015 15:07:29 (UTC+8)-
dc.date.available 17-Jun-2015 15:07:29 (UTC+8)-
dc.date.issued (上傳時間) 17-Jun-2015 15:07:29 (UTC+8)-
dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/75882-
dc.description.abstract (摘要) We present a Hindley/Milner-style polymorphic type system for var, an extension of the call-by-name -calculus with mutable variables and assignments. To match var`s explicit distinction between functional and imperative worlds, the type universe is stratified into two layers: one for applicative expressions and one for imperative state transformers. In inferring types for var-terms, the type system performs a simple effect analysis to statically verify the safety of coercing a state transformer to a pure value. We prove the soundness of the type system with respect to var`s untyped reduction semantics so that any well-typed program will evaluate to an answer, provided the evaluation terminates. We also discuss some practical aspects of the type system and present a type checker based on the well-known W algorithm.
dc.format.extent 124 bytes-
dc.format.mimetype text/html-
dc.relation (關聯) Theoretical Aspects of Computer Software - TACS , pp. 347-364
dc.title (題名) A Type System for a Lambda Calculus with Assignments
dc.type (資料類型) articleen
dc.identifier.doi (DOI) 10.1007/3-540-57887-0_103
dc.doi.uri (DOI) http://dx.doi.org/10.1007/3-540-57887-0_103