TY - GEN
T1 - A rewriting semantics for type inference
AU - Kuan, George
AU - MacQueen, David
AU - Findler, Robert Bruce
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=37149009050&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=37149009050&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-71316-6_29
DO - 10.1007/978-3-540-71316-6_29
M3 - Conference contribution
AN - SCOPUS:37149009050
SN - 354071314X
SN - 9783540713142
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 426
EP - 440
BT - Programming Languages and Systems - 16th European Symposium on Programming, ESOP 2007. Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Proceedings
PB - Springer Verlag
T2 - 16th European Symposium on Programming, ESOP 2007
Y2 - 24 March 2007 through 1 April 2007
ER -