A Framework for Implementing Type Systems
				  by
		    Brian Dorn and Gary T. Leavens

			       Abstract

Type systems are ubiquitous in the study of programming languages.
Although the basic mechanisms are well understood, 
a new type system can still be a challenge to implement.
We present the design and implementation of a domain-specific language
(i.e., a functional framework) for writing type system implementations.
This domain-specific language has been embedded in both Haskell and
Scheme.  It allows users to write down the axioms and inference
rules of the type system in a stylized notation that closely resembles
the formal type rules, and automates the rest of the work of type
checking or type inference.

Keywords: Type inference, type checking, Scheme language, Typedscm language.

2006 CR Categories:
D.2.13 Software Engineering
     Reusable Software --- reusable libraries;
D.3.2 Programming Languages
    Language Classifications --- applicative (functional) languages, Scheme.