Colored Local Type Inference (colored version). (black and white version). Martin Odersky, Christoph Zenger, Matthias Zenger.POPL 2001, January 2001. Abstract. We present a type system for a language based on F-sub, which allows certain type annotations to be elided in actual programs. Local type inference determines types by a combination of type propagation and local constraint solving, rather than by global constraint solving. We refine the previously existing local type inference system of Pierce and Turner[Local Type Inference, POPL 98] by allowing partial type information to be propagated. This is expressed by coloring types to indicate propagation directions. Propagating partial type information allows us to omit type annotations for the visitor pattern, the analogue of pattern matching in languages without sum types.

Indizierte Typen. Christoph Zenger. Doctoral Dissertation, July 1998.

Indexed Types. Christoph Zenger. Draft translation of some chapters of the above thesis.

Indexed Types. Christoph Zenger. Theoretical Computer Science 187:147-165, 1997. Abstract. A new extension of the Hindley/Milner type system is proposed. The type system has algebraic types, that have not only type parameters, but also value parameters (indices). This allows for example to parameterize matrices and vectors by their size and to check size compatibility statically. This is especially of interest in computer algebra.

Nested Types. Martin Odersky and Christoph Zenger. FOOL8, January 2001.

A Functional View Of Join. Gang Chen, Martin Odersky, Christoph Zenger, Matthias Zenger. Technical Report ACRC-99-016, University of South Australia 1999. Abstract. Join calculus, usually presented as a process calculus, is suitable as a foundation of both sequential and concurrent programming. We give a new operational semantics of join calculus, expressed as a reduction system with a single reduction rule similar to beta reduction in lambda calculus. We also introduce a new Hindley/Milner style type system for join calculus. Compared to previous work, the type system gives more accurate types of composite and mutually recursive definitions. The type system's soundness is established by showing that our reduction rule keeps typings invariant. We present an algorithm for type inference and show its soundness and completeness.

Hindley/Milner Style Type Systems in Constraint Form. Martin Sulzmann, Martin Müller, Christoph Zenger. Technical Report ACRC-99-009, University of South Australia 1999. Abstract. This paper describes Hindley/Milner style type systems in constraint form. Previously, many type descriptions have still been partially represented in the type language. We argue that this can lead to shortcomings in the type and inference system. Examples are given to support this statement. As a solution we present a purely constraint-based formulation of Hindley/Milner style type systems which enjoys much nicer logical properties than previous approaches. More specifiacally we present a solution to the open problem of type inference in non-regular theories.