scholarly journals A mechanical formalization of higher-ranked polymorphic type inference

2019 ◽  
Vol 3 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Jinxu Zhao ◽  
Bruno C. d. S. Oliveira ◽  
Tom Schrijvers
Keyword(s):  
Type Inference ◽  
Polymorphic Type

Sound polymorphic type inference for objects

1995 ◽  
Vol 30 (10) ◽  
pp. 169-184 ◽  
Author(s):  
Jonathan Eifrig ◽  
Scott Smith ◽  
Valery Trifonov
Keyword(s):  
Type Inference ◽  
Polymorphic Type

Proofs of a set of hybrid let-polymorphic type inference algorithms

2004 ◽  
Vol 22 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Hyunjun Eo ◽  
Oukseh Lee ◽  
Kwangkeun Yi
Keyword(s):  
Type Inference ◽  
Inference Algorithms ◽  
Polymorphic Type

scholarly journals A Type Inference Algorithm for a Stratified Polymorphic Type Discipline

1994 ◽  
Vol 109 (1-2) ◽  
pp. 115-173 ◽  
Author(s):  
P. Giannini ◽  
S.R. Dellarocca
Keyword(s):  
Type Inference ◽  
Inference Algorithm ◽  
Polymorphic Type

FIRST-CLASS CONTEXTS IN ML

2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO
Keyword(s):  
Programming Language ◽  
Operational Semantics ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Hole Filling ◽  
Dynamic Binding ◽  
Polymorphic Type ◽  
Open Program ◽  
Program Modules

This paper develops an ML-style programming language with first-class contexts i.e. expressions with holes. The crucial operation for contexts is hole-filling. Filling a hole with an expression has the effect of dynamic binding or macro expansion which provides the advanced feature of manipulating open program fragments. Such mechanisms are useful in many systems including distributed/mobile programming and program modules. If we can treat a context as a first-class citizen in a programming language, then we can manipulate open program fragments in a flexible and seamless manner. A possibility of such a programming language was shown by the theory of simply typed context calculus developed by Hashimoto and Ohori. This paper extends the simply typed system of the context calculus to an ML-style polymorphic type system, and gives an operational semantics and a sound and complete type inference algorithm.

Weak polymorphism can be sound

1996 ◽  
Vol 6 (1) ◽  
pp. 111-141 ◽  
Author(s):  
John Greiner
Keyword(s):  
New Jersey ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Inference Algorithm ◽  
Standard Ml ◽  
Polymorphic Type

AbstractThe weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.

scholarly journals Polymorphic Type Inference for the Relational Algebra

2002 ◽  
Vol 64 (3) ◽  
pp. 694-718 ◽  
Author(s):  
Jan Van den Bussche ◽  
Emmanuel Waller
Keyword(s):  
Type Inference ◽  
Relational Algebra ◽  
Polymorphic Type
Sign in / Sign up

Export Citation Format

Share Document