A Framework for Implementing Type Systems

Dorn, Brian and Leavens, Gary T. (2007) A Framework for Implementing Type Systems. Technical Report TR#07-12, Computer Science, Iowa State University.

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.