A Rewriting Logic Approach to Defining Type Systems

Ellison, Chucky M.

Permalink

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

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

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