IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

A Rewriting Logic Approach to Defining Type Systems

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/18078

Files in this item

File Description Format
PDF ellison-2008-mastersthesis.pdf (532KB) Main article PDF
Title: A Rewriting Logic Approach to Defining Type Systems
Author(s): Ellison, Chucky M.
Advisor(s): Roşu, Grigore
Department / Program: Computer Science
Discipline: Computer Science
Degree Granting Institution: University of Illinois at Urbana-Champaign
Degree: M.S.
Genre: Thesis
Subject(s): Rewriting Logic type systems preservation and progress soundness
Abstract: We show how programming language semantics and definitions of their corresponding type systems can both be written in a single framework amenable to proofs of soundness. The framework is based on full rewriting logic (not to be confused with context reduction or term rewriting), where rules can match anywhere in a term (or configuration). We present an extension of the syntactic approach to proving type system soundness presented by Wright and Felleisen [1994] that works in the above described semantics-based domain. As before, the properties of preservation and progress are crucial. We use an abstraction function to relate semantic configurations in the language domain to semantic configurations in the type domain, and then proceed to use the preservation and progress properties as usual. We also develop an abstract type system, which is a type system modulo certain structural characteristics. To demonstrate the method, we give examples of five languages and corresponding type systems. They include two imperative languages and three functional languages, and three type checkers and two type inferencers. We then proceed to prove that preservation holds for each.
Issue Date: 2008
Citation Info: @mastersthesis{ellison-2008-mastersthesis, title = "A Rewriting Logic Approach to Defining Type Systems", author = "{Ellison III}, Charles M.", year = "2008", school = "University of Illinois at Urbana-Champaign", note = "\url{http://hdl.handle.net/2142/18078}", }
Genre: Technical ReportDissertation / Thesis
Type: Text
Language: English
URI: http://hdl.handle.net/2142/18078
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2010-12-31
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 83
  • Downloads this Month: 1
  • Downloads Today: 0

Browse

My Account

Information

Access Key