Proofs of a set of hybrid let-polymorphic type inference algorithms |
| |
Authors: | Email author" target="_blank">Hyunjun?EoEmail author Oukseh?Lee Kwangkeun?Yi |
| |
Affiliation: | (1) Research On Program Analysis System Department of Computer Science, Korea Advanced Institute of Science and Technology, 373-1 Guseong-dong, Yuseong-gu, 305-701 Daejeon, Korea;(2) School of Computer Science and Engineering, Seoul National University, San 56-1, Shilim-dong, Gwanak-gu, 151-742 Seoul, Korea |
| |
Abstract: | We present a generalized let-polymorphic type inference algorithm, prove that any of its instances is sound and complete with
respect to the Hindley/Milner let-polymorphic type system, and find a condition on two instance algorithms so that one algorithm
should find type errors earlier than the other.
By instantiating the generalized algorithm with different parameters, we can obtain not only the two opposite algorithms (the
bottom-up standard algorithmW and the top-down algorithmM) but also other hybrid algorithms which are used in real compilers. Such instances’ soudness and completeness follow automatically,
and their relative earliness in detecting type-errors is determined by checking a simple condition. The set of instances of
the generalized algorithm is a superset of those used in the two most popular ML compilers: SML/NJ and OCaml.
This work is supported by Creative Research Initiatives of the Korean Ministry of Science and Technology
National Creative Research Initiative Center, http://ropas.kaist.ac.kr
Work done while the third author was associated with Korea Advanced Institute of Science and Technology
Hyunjun Eo: He is a Ph.D. candidate in the Department of Computer Science at KAIST (Korea Advanced Institute of Science and Technology).
He recieved his bachelor’s degree and master’s degree in Computer Science from KAIST in 1996 and 1998, respectively. His research
interest has been on static program analysis, fixpoint iteration algorithm and higher-order and typed languages. From fall
1998, he has been a research assistant of the National Creative Research Initiative Center for Research on Program Analysis
System. He is currently working on developing a tool for automatic generation of program analyzer.
Oukseh Lee: He is a Ph.D. candidate in the Department of Computer Science at KAIST (Korea Advanced Institute of Science and Technology).
He received his bachelor’s and master’s degree in Computer Science from KAIST in 1995 and 1997, respectively. His research
interest has been on static program analysis, type system, program language implementation, higher-order and typed languages,
and program verification. From 1998, he has been a research assistant of the National Creative Research Initiative Center
for Research on Program Analysis System. He is currently working on compile-time analyses and verification for the memory
behavior of programs.
Kwangkeun Yi, Ph.D.: His research interest has been on semanticbased program analysis and systems application of language technologies. After
his Ph.D. from University of Illinois at Urbana-Champaign he joined the Software Principles Research Department at Bell Laboratories,
where he worked on various static analysis approaches for higher-order and typed programming languages. For 1995 to 2003 he
was a faculty member in the Department of Computer Science, Korea Advanced Institute of Science and Technology. Since fall
2003, he has been a faculty member in the School of Computer Science and Engineering, Seoul National University. |
| |
Keywords: | Type System Type Inference Algorithm Let-Polymorphism Generalization |
本文献已被 SpringerLink 等数据库收录! |
|