A rewriting logic approach to type inference

Chucky Ellison, Traian Florin Şerbǎnuţǎ, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Meseguer and Roşu proposed rewriting logic semantics (RLS) as a programing 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 define 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. The proposed approach is exemplified by defining the Hindley-Milner polymorphic type inferencer W as a rewrite logic theory and using this definition to obtain a type inferencer by executing it in a rewriting logic engine. The inferencer obtained this way compares favorably with other definitions or implementations of W. The performance of the executable definition is within an order of magnitude of that of highly optimized implementations of type inferencers, such as that of OCaml.

Original languageEnglish (US)
Title of host publicationRecent Trends in Algebraic Development Techniques - 19th International Workshop, WADT 2008, Revised Selected Papers
Number of pages17
StatePublished - 2009
Event19th International Workshop on Algebraic Development Techniques, WADT 2008 - Pisa, Italy
Duration: Jun 13 2008Jun 16 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5486 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other19th International Workshop on Algebraic Development Techniques, WADT 2008

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A rewriting logic approach to type inference'. Together they form a unique fingerprint.

Cite this