… The fundamental purpose of a type system is to prevent the occurrence … the study of type systems, but requires clarification. Its accuracy depends … of type systems has emerged as a formal discipline. …
In Allen B. Tucker, editor, The Computer Science and Engineering Handbook. pages 2208-2236, CRC Press, 1997.… A practical type system for ML-style recursive modules should address at least … definitions caused by recursion between modules. Although type systems in previous … of recursive modules. This paper proposes a novel type system for recursive …
OOPSLA 2011: 993-1012 [doi]… We present a general framework HM(X) for type systems with constraints. The framework stays in the tradition of the Hindley/Milner type system. Its type system … give a generic type inference algorithm for HM(X) so that, under sufficient …
tapos, 5(1):35-55, 1999.… This papers describes Hindley/Milner stype type systems in constraint form. Previously, many type descriptions have still been partially represented … a purely constraint based formulation of Hindley/Milner style type systems …
Technical Report ACRC–99–009, 1999.… The correct definition and implementation of non-trivial type systems … that simplifies the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries …
OOPSLA 2015: 137-150 [doi]… We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class values. Our type system harmonizes design …
POPL 2003: 236-249 [doi]… In this paper we describe a type system for a generative mechanism that generalizes the concept of generic types by combining it with a controlled form … generic types alone would be insufficient. The power of code generation features …
GPCE 2005: 327-341 [doi]… We present Turnstile, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling … reuse. It exploits a macro system in a novel way to simultaneously type check …
POPL 2017: 694-705 [doi]… Type systems are aimed at preventing programming language constructions from … that a type system is well defined. However, the type systems implemented … a specification of the type system as its input. The generated code interacts with an API …
Lecture Notes on Software Engineering, 2(4):288-293, 2014. [doi]… Type theories in the sense of Martin-Löf and the NuPRL system are based on taking as primitive a type-free programming language given by an operational … terms. The construction of a type system is based on a general form of inductive …
JSC, 14(1):71-84, 1992.… Reynolds’ abstraction theorem shows how a typing judgement in System F can …, and their relations are expressed in a single typed lambda calculus (a pure type system … constraints on the type system (which we spell out), the result applies to many …
ICFP 2010: 345-356 [doi]… of program variants grows exponentially with the number of features, we cannot type-check each variant on its own. Recently, product-line-aware type systems were … Java in Coq. Furthermore, we present a simpli ed type system for Colored …
Master's thesis, University of Magdeburg, Germany, January 2010.… with a type system that enforces a unicity property for location names …
fmoods 2003: 109-123 [doi]… Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy … features of the type system, and as a platform from which to explore new …
In Haskell Workshop. 1999: [doi]… for a language, our system automatically checks type soundness by checking … contributions both in the area of checking soundness of type systems, and in the area …This paper presents novel techniques for checking the soundness of a type …
OOPSLA 2008: 493-504 [doi]… Some type systems are first described formally, to be sometimes followed by an implementation. Other type systems are first implemented as language extensions … be incrementally described, thus providing a means for building complex type systems on top …
FLOPS 2006: 30-46 [doi]… language because its features cannot be captured fully by a static type system … for optimization.
In this paper, we introduce a gradual type system … checks (casts). The type system is backwards compatible such that types can …
SLE 2020: 1-15 [doi]… We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function … show that type reconstruction in this system can be reduced to the decidable …
POPL 1996: 54-67 [doi]