| dc.contributor | 資科系 | |
| dc.creator (作者) | Chen, Kung;Odersky, Martin | |
| dc.creator (作者) | 陳恭 | zh_TW |
| dc.date (日期) | 1994 | |
| dc.date.accessioned | 17-六月-2015 15:07:29 (UTC+8) | - |
| dc.date.available | 17-六月-2015 15:07:29 (UTC+8) | - |
| dc.date.issued (上傳時間) | 17-六月-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 (資料類型) | article | en |
| 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 | |
