Award Date

12-1-2022

Degree Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Computer Science

First Committee Member

Jan Pedersen

Second Committee Member

Kazem Taghva

Third Committee Member

Fatma Nasoz

Fourth Committee Member

Andreas Stefik

Fifth Committee Member

John Minor

Sixth Committee Member

Laxmi Gewali

Abstract

Type systems are a key characteristic in the context of the study of programming languages. They frequently offer a simple, intuitive way of expressing and testing the fundamental structure of programs. This is especially true when types are used to provide formal, machine-checked documentation for an implementation. For example, the absence of type errors in code prior to execution is what type systems for static programming languages are designed to assure, and in the literature, type systems that satisfy this requirement are referred to as sound type systems. Types also define module interfaces, making them essential for achieving and maintaining consistency in large software systems. On these accounts, type systems can enable early detection of program errors and vastly improve the process of understanding unfamiliar code. However, even for verification professionals, creating mechanized type soundness proofs using the tools and procedures readily available today is a difficult undertaking. Given this result, it is only logical to wonder if we can capture and check more of the program structure, so the next two questions concern type checking. Once a type system has been specified, how can we implement a type checker for the language? Another common question concerns the operational semantics, that is, once the type system is specified, how can we take advantage of this specification to obtain a type checker for the language? In each of these cases, type systems are often too complex to allow for a practical and reasonable approach to specifying many common language features in a natural fashion; therefore, the crux here is: What is the bare minimum set of constructs required to write a type checker specification for any domain-specific language (DSL)? We believe that sets (including tests for memberships, subsets, size, and other properties) as well as first-order logic and an expression grammar can be used to do this. In addition, we will need the ability to apply some form of filter on sets, as well as possibly a reduction and map. The primary goal of this thesis is to raise the degree of automation for type checking, so we present Jiapi, an automatic type checker generation tool. The tool generates a type checker based on a description of a language’s type system expressed in set notation and first-order logic, allowing types to be interpreted as propositions and values to be interpreted as proofs of these propositions, which we can then reduce to a small number of easily-reviewable predicates. Consequently, we can have a completely spelled-out model of a language’s type system that is free of inconsistencies or ambiguities, and we can mathematically demonstrate features of the language and programs written in it. We use two languages as case studies: a somewhat large and more general, and a more domain-specific. The first one is a true subset of Java (an object-oriented language) called Espresso, and the second one is a pedagogical language like C/C++ called C-Minor. Also, there is a declarative type system description extension for the first language, and parts of the specification for the second one. Finally, our approach is evaluated to demonstrate that the generated type checker can check automatically the full functional correctness of an Espresso and C-Minor program.

Keywords

compilers; domain-specific languages; programming languages; statically typed languages; Type checking; type systems

Disciplines

Computer Sciences

File Format

pdf

File Size

3000 KB

Degree Grantor

University of Nevada, Las Vegas

Language

English

Rights

IN COPYRIGHT. For more information about this rights statement, please visit http://rightsstatements.org/vocab/InC/1.0/

Download


Share

COinS