Type Theoretic Properties of Assignments

159 p.Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1992.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.U of I OnlyRestricted to the U of I community idenfinitely during batch ingest of legacy ETD