… 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
… 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
… 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
… 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
… 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
… 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.
… 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.
… 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.
… 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
… with a type system that enforces a unicity property for location names …fmoods 2003: 109-123
… 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:
… 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
… 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
… 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
… 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