Paper Info
Title
A rewriting semantics for type inference
Abstract
When students first learn programming, they often rely on a simple operational model of a program's behavior to explain how particular features work. Because such models build on their earlier training in algebra, students find them intuitive, even obvious. Students learning type systems, however, have to confront an entirely different notation with a different semantics that many find difficult to understand. In this work, we begin to build the theoretical underpinnings for treating type checking in a manner like the operational semantics of execution. Intuitively, each term is incrementally rewritten to its type. For example, each basic constant rewrites directly to its type and each lambda expression rewrites to an arrow type whose domain is the type of the lambda's formal parameter and whose range is the body of the lambda expression which, in turn, rewrites to the range type.
Year
DOI
Venue
2007
10.1007/978-3-540-71316-6_29
ESOP
Keywords
Field
DocType
lambda expression rewrite,different semantics,arrow type,type inference,type checking,lambda expression,particular features work,operational semantics,range type,different notation,type system,model building
Void type,Hindley–Milner type system,Operational semantics,Programming language,Unit type,Computer science,Type erasure,Type inference,Theoretical computer science,Rewriting,Recursive data type
Conference
Volume
ISSN
Citations 
4421
0302-9743
11
PageRank 
References 
Authors
0.70
18
3
Name
Order
Citations
PageRank
George Kuan1151.45
David B. MacQueen2850229.37
Robert Bruce Findler390467.67