Files in this item



application/pdfellison-2008-mastersthesis.pdf (532kB)
Main articlePDF


Title:A Rewriting Logic Approach to Defining Type Systems
Author(s):Ellison, Chucky M.
Advisor(s):Rosu, Grigore
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Rewriting Logic
type systems
preservation and progress
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{}", }
Genre:Technical Report
Dissertation / Thesis
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2010-12-31

This item appears in the following Collection(s)

Item Statistics