TY - GEN
T1 - A rewriting logic approach to type inference
AU - Ellison, Chucky
AU - Şerbǎnuţǎ, Traian Florin
AU - Roşu, Grigore
N1 - Funding Information:
Supported in part by NSF grants CCF-0448501, CNS-0509321 and CNS-0720512, by NASA contract NNL08AA23C, by the Microsoft/Intel funded Universal Parallel Computing Research Center at UIUC, and by several Microsoft gifts.
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70349333898&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349333898&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-03429-9_10
DO - 10.1007/978-3-642-03429-9_10
M3 - Conference contribution
AN - SCOPUS:70349333898
SN - 3642034284
SN - 9783642034282
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 135
EP - 151
BT - Recent Trends in Algebraic Development Techniques - 19th International Workshop, WADT 2008, Revised Selected Papers
T2 - 19th International Workshop on Algebraic Development Techniques, WADT 2008
Y2 - 13 June 2008 through 16 June 2008
ER -