A Rewriting Logic Approach to Type Inference

Date Added: Feb 2010
Format: PDF

Meseguer and Rosu proposed Rewriting Logic Semantics (RLS) as a programming language definitional framework that unifies operational and algebraic denotational semantics. RLS has already been used to define a series of didactic and real languages, but its benefits in connection with defining and reasoning about type systems have not been fully investigated. This paper shows how the same RLS style employed for giving formal definitions of languages can be used to de ne type systems. The same term-rewriting mechanism used to execute RLS language definitions can now be used to execute type systems, giving type checkers or type inferencers.