… give a generic type inference algorithm for HM(X) so that, under sufficient conditions on X, type inference will always compute the principal type of a term. We …We present a general framework HM(X) for type systems with constraints …
tapos, 5(1):35-55, 1999.… in the constraint domain X. Type inference is performed by generating … constraint solver X. The solver has to be invoked at the latest when type inference … approach where the HM(X) type inference problem is first mapped to a CLP(X) program …
JFP, 18(2):251-283, 2008. [doi]… us to make important distinctions between different phases of type inference … naturally by employing a constraint-based view of type inference. In addition, our formulation of type inference can easily be tailored to different inference …
FLOPS 2001: 248-263 [doi]… strongly depends on the precision of the underlying type inference algorithm. Previous work on type inference for Datalog has focussed on Cartesian abstractions, where the type of each field is computed separately. Such Cartesian type inference …
PODS 2008: 291-300 [doi]… We present a unified approach to type inference in the presence of overloading …. We prove the decidability of type inference for the class of decomposable … inference system, show that subtyping and overloading can be treated as a special …
lfp 1992: 193-204 [doi]… We study two partial type inference methods for a language combining subtyping … inference in a sizable body of existing ML code. … method infers type arguments in polymorphic applications using a local constraint …
TOPLAS, 22(1):1-44, 2000. [doi]… for easy extensibility to other type inference problems. … a term of the untyped lambda calculus is the image under type-erasing of a term of the simply typed lambda calculus. The proof proceeds by a direct reduction …
Fundamenta Infomaticae, 10:115-122, 1987.… inference system is consistent with an operational dynamic semantics …Three languages with polymorphic type disciplines are discussed, namely the λ-calculus with Milner’s polymorphic type discipline; a language with imperative …
, 1988.… , we obtain the result that type/effect inference in our system is polynomial-time …We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one …
ENTCS, 242(3):21-36, 2009. [doi]… is known. Two approaches to do this are abstract interpretation and type inference … on closure analysis and the second is the type inference approach of Gomard …
iccl 1994: 277-288 [doi]… inference when they are used as local type assumptions. Local type assumptions often … inference approach for local type assumptions. Our system, called OutsideIn(X … as HM(X). This stratification allows us to use a common metatheory and inference …
J. Funct. Program., 21(4-5):333-412, 2011.… Type inferencing according to the standard algorithms W and M often yields unin- formative error messages. Many times, this is a consequence of a bias inherent … the correctness for W and M with respect to the Hindley-Milner typing rules for free …
Technical Report UU-CS-2002-031, 2002.… the type system, prove its safety and define a type inference algorithm which … the non-standard construct of the constraint language generated by type inference … inference framework, with bounded existential (a.k.a. abstract) and universal …
SIGPLAN, 38(9):39-50, 2003. [doi]… and more recently in a type-theoretic setting. In a type-theoretic setting binding-time analysis is a type inference problem: the problem of inferring … core of type inference for binding-time analysis in Gomard’s type system …
fpca 1991: 448-472 [doi]… Inference of static types for local variables in Java bytecode is the first … finding a set of minimal typings that are valid for all assignments, and then checking whether these minimal typings satisfy all uses. Unlike previous algorithms …
OOPSLA 2008: 475-492 [doi]… this without sacrificing type inference. We present a new type system for higher-rank … a complete and decidable type inference algorithm. … polymorphic types may occur. Supporting ``first-class'' polymorphism, by lifting …
ICFP 2008: 295-306 [doi]… intuitive, even obvious. Students learning type systems, however, have to confront … for treating type checking in a manner like the operational semantics of execution. Intuitively, each term is incrementally rewritten to its type …
ESOP 2007: 426-440 [doi]