Type Theories in ML

Type Theories in ML
**David A. Schmidt, Allen Stoughton, Brian T. Howard. Kansas State University (N00014-94-1-0866)**
	Objectives: development of programming methodology for construction of correct, modular programs in ML-like languages formalization of foundations of program analysis and verification
Approaches: Implementation of Languages and Tools: use constructive type theory and intuitionistic logic as basis for languages and tools to support programming methodology Foundational Research: apply abstract interpretation to formalize program analysis based on formal semantics	Results: lemon, an ML-like language with inductive and coinductive types porgi, a Proof-Or-Refutation-Generator for Intuitionistic propositional logic a methodology for programming with induction and coinduction coinductive natural semantics, a formal semantics for programs with infinite data structures and control

Narrative for slide: quadrant 1 (picture)

The programming languages research group at Kansas State University wants to write software as sound and secure as the building that they are housed in! (By the way, the building is Nichols Hall; it was built in 1914 and housed the University's gymnasium and ROTC program prior to its occupancy by its current residents, the computer science department.) For this reason, the group studies applications of logic to the development of correct, modular software

Narrative for slide: quadrant 2 (Objectives)

Large systems are built in modular components, and the key to building correct systems is ensuring the correctness of the interconnections of the components. The primary objective of the project, ``Type Theories in ML,'' is to develop a programming methodology and support tools for programming individual modules correctly and linking modules together correctly. ML-like languages have been chosen for the research because ML is a statically typed language, which makes it amenable to compile-time and link-time verification, and ML already possesses a rich typing system that makes it easier to integrate program validation activities with type checking.
A second objective of the project is to formalize and adapt the foundations of program analysis to verification. The starting point is data-flow analysis: data-flow analysis techniques have proved highly successful in optimizing compilers. The underlying theory of data flow analysis is called abstract interpretation, and the Kansas group is adapting abstract interpretation to program verification. The goal is to use abstract interpretation to simplify or automate some of the simpler verification activities.

Narrative for slide: quadrant 3 (Approaches)

The research has been approached along two lines:

The first line of research is concerned with implementing languages and tools to support correct programming. Not surprisingly, formal logic is used as the starting point: constructive type theory provides a rich and sound theory for data and control structures, and its associated logic makes possible correctness proofs for code. For this reason, an implementation of an ML-variant programming language based on constructive type theory is used as the starting language. Support tools for verification checking of program code and linkages have also been developed. Implementations are undertaken as an integral part of the research: they ensure that intuitions and formal results actually work in practice.
The second line of research has been upon the foundations of abstract interpretation. Stated roughly, abstract interpretation is an algebraic approach to programming language analysis, where the semantics of a programming language as well as its data-flow analysis are homomorphisms, and the correctness of the data-flow analysis is ensured by a Galois connection between the target algebras of the semantics and the data-flow analysis. Abstract interpretation has worked best at explaining traditional dataflow analysis of first-order programming languages, and the research done here is dedicated to extending abstract interpretation to nonstandard languages and problem domains.

Narrative for slide: quadrant 4 (Results)

One of the initial accomplishments of the project is the design and implementation of lemon, an ML-like language augmented by the structures of constructive type theory. These additional structures, called inductive and coinductive types, allow correctness proofs based on classic induction and more novel coinduction techniques. In addition, lemon supports a division of language features into provably ``safe'' and ``unsafe'' categories, so that the programmer is aware of which portions of a program are secure and which parts are potentially insecure. These results are documented in Howard's paper, ``Inductive, coinductive, and pointed types'' (Proc. 1996 ACM SIGPLAN International Conference on Functional Programming).
In tandem with lemon, a proof-or-refutation-generator, porgi, was developed. Porgi is a program generator for propositional intuitionistic logic: if a proposition is provable in propositional intuitionistic logic, porgi builds a proof and generates a lemon program that is an encoding of the proof. Conversely, if the proposition is unprovable, progi produces a Kripke-style model that refutes the proposition. Aside from its value as a testing tool for the lemon interpreter, porgi is of interest as a theorem prover for intutionistic propositional logic. The system is documented in Stoughton's paper, ``porgi: A Proof-Or-Refutation Generator for Intuitionistic propositional logic'' (submitted to the 13th Conference on Automated Deduction). A linker tool has also been developed for lemon modules, although the results here are preliminary.
In addition to implementation work, an experiment on programming with inductive and coinductive types was undertaken by systematically redeveloping sorting algorithms. It was discovered that the standard algorithms---insertion sort, merge sort, selection sort, and quick sort---arise naturally as a result of choice of inductive or coinductive programming strategy, suggesting that standard solutions to standard programming problems can be derived in similar ways. The experiment is documented in Howard's paper, ``Another iteration on Darlington's `A synthesis of several sorting algorithms' '' (Acta Informatica, to appear).
Finally, the foundations of abstract interpretation were extended by adapting it to operate on coinductively defined natural semantics. Natural semantics is a form of operational semantics where a program's execution is written as a proof derivation; in coinductive natural semantics, the proof derivation can be infinite. An abstract interpretation of such an infinite derivation is another potentially infinite derivation where run-time data are replaced by properties. Termination of the abstract interpretation is guaranteed by truncating infinite paths in the derivation where ``repetitions'' occur. This approach naturally adapts to the inductive and coinductive structures of lemon programs. The material is documented in Schmidt's paper, ``Natural-semantics-based abstract interpretation,'' (Proc. 2d Static Analysis Symposium).