This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/72060
Description
Title
Type Theoretic Properties of Assignments
Author(s)
Swarup, Vipin
Issue Date
1992
Doctoral Committee Chair(s)
Kamin, S.N.,
Reddy, U.S.,
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Abstract
This thesis is concerned with extending the correspondence between intuitionistic logic and functional programming to include assignments and dynamic data. We propose a theoretical framework for adding these imperative features to functional languages without violating their semantic properties. We also describe a constructive programming logic that embodies the principles for reasoning about the extended language.
We present an abstract formal language, called Imperative Lambda Calculus (ILC), that extends the typed lambda calculus with imperative programming features, namely references and assignments. The language shares with typed lambda calculus important properties such as the Church-Rosser property and strong normalization. Thus, programs produce the same results with eager and lazy evaluation orders. ILC permits mutable data structures such as arrays, linked lists, trees, and graphs to be constructed and used. Shared values may be updated destructively rather than by copying. This permits pure functional languages to have efficient implementations of problems such as topological sort, graph reduction, and unification.
We describe the logical symmetries that underlie ILC by exhibiting a constructive logic, called Observation Type Theory (OTT), for which ILC forms the language of constructions. Central to this formulation is the view that references play a role similar to that of variables. References can be used to range over values and can be instantiated to specific values. Thus, we obtain a new form of universal quantification that uses references instead of variables. The term forms of ILC are then obtained as the constructions for the introduction and elimination of this quantifier. While references duplicate the role of variables, they also have important differences. References are semantic values whereas variables are syntactic entities; further, references are reusable. These differences allow us to use references in a more flexible fashion, leading to efficiency in constructions and algorithms.
Finally, we describe a higher-order type theory, namely the Nuprl type theory, and illustrate how its inductive types can be used to define well-founded orderings. These can then be used to construct recursive programs.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
