A rewriting semantics for type inference

George Kuan*, David MacQueen, Robert Bruce Findler

*Corresponding author for this work

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

9 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationProgramming 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
PublisherSpringer Verlag
Number of pages15
ISBN (Print)354071314X, 9783540713142
StatePublished - 2007
Event16th European Symposium on Programming, ESOP 2007 - PRT, Portugal
Duration: Mar 24 2007Apr 1 2007

Publication series

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


Other16th European Symposium on Programming, ESOP 2007

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A rewriting semantics for type inference'. Together they form a unique fingerprint.

Cite this