University of Illinois Urbana-Champaign

A Rewriting Logic Approach to Defining Type Systems

Ellison, Chucky M.

Content Files
ellison-2008-mastersthesis.pdf

Permalink

https://hdl.handle.net/2142/18078

Description

Title
A Rewriting Logic Approach to Defining Type Systems
Author(s)
Ellison, Chucky M.
Issue Date
2008
Director of Research (if dissertation) or Advisor (if thesis)
Rosu, Grigore
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Date of Ingest
2010-12-31T19:34:50Z
Keyword(s)
  • Rewriting Logic
  • type systems
  • preservation and progress
  • soundness
Language
en
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.
Type of Resource
text
Permalink
http://hdl.handle.net/2142/18078

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Siebel School of Computer Science