A Rewriting Logic Approach to Type Inference

Ellison, Chucky M.; Serbanuta, Traian Florin; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11423 Copy

Description

Title

A Rewriting Logic Approach to Type Inference

Author(s)

• Ellison, Chucky M.
• Serbanuta, Traian Florin
• Rosu, Grigore

Issue Date

2008-03

Keyword(s)

programming languages

Abstract

"Meseguer and Rosu proposed rewriting logic semantics (RLS) as a programming language definitional framework that unifies operational and algebraic denotational semantics. Once a language is defined as an RLS theory, many generic tools are immediately available for use with no additional cost to the designer. These include a formal inductive theorem proving environment, an efficient interpreter, a state space explorer, and even a model checker. 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 yet. 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. Since both the language and its type system are defined uniformly as theories in the same logic, one can use the standard RLS proof theory to prove properties about languages and type systems for those languages. The proposed approach is exemplified by defining Milner's polymorphic type inferencer W as a rewrite logic theory and using the definition: (1) to prove its soundness using Wright and Felleisen's standard preservation and progress methodology, and (2) to obtain a type inferencer by executing the definition in the Maude rewrite engine. The inferencer obtained ""for free"" was tested against implementations used in some current functional languages. It was found to be quite competitive---for example, it outperformed SML's type inferencer in all experiments. To show that the proposed rewriting approach and the resulting type inferencers scale, Milner's simple language is extended with multiple-binding let and letrec, with lists, and with references and side effects. The resulting type inferencer, able to detect weak polymorphism, is only slightly slower than the one for Milner's simpler language. No proofs are given for the extended type system."

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11423

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections