Author: Nazareth Karjian
The similarity between mathematical proofs and computer programs has recently received increased emphasis. This report presents a proof checker for the propositional and predicate logics. It shows how programming language design techniques can be employed in the analysis and verification of proofs. We devise a proof language and construct a compiler in Standard ML to illustrate, with an actual system, how the techniques apply. The result is an automated system that is especially useful as a tool for expressing and verifying large proofs.
Authors: Anindya Banerjee and David A. Schmidt
We present static criteria to determine when higher-order functional programs can be implemented on a machine with a single, global environment stack. Our criteria use the lambda-abstraction as a block-structuring concept for controlling the extents of bindings in the environment.
Author: Brian T. Howard
In ``A synthesis of several sorting algorithms'' [J. Darlington, Acta Informatica 11:1-30, 1978], Darlington showed how to use program transformation techniques to develop versions of six well-known sorting algorithms. The purpose of this note is to provide more evidence for the naturalness of the resulting taxonomy of algorithms by showing how it follows almost immediately from a consideration of the types of the objects involved. By exploiting the natural operations of iteration and coiteration over recursively defined data types, we may automatically derive much of the structure of each algorithm.
Author: Brian T. Howard
An extension of the simply-typed lambda calculus is presented which contains both well-structured inductive and coinductive types, and which also identifies a class of types for which general recursion is possible. The motivations for this work are certain natural constructions in category theory, in particular the notion of an algebraically bounded functor, due to Freyd. We propose that this is a particularly elegant language in which to work with recursive objects, since the potential for general recursion is contained in a single operator which interacts well with the facilities for bounded iteration and coiteration.
Author: David Schmidt
The original formulation of abstract interpretation (a.i.) by Cousot and Cousot demonstrated clearly that a.i. is a formal-semantics-based methodology for deriving a provably correct, convergent, canonical iterative data flow analysis from a standard semantics of a programming language. But subsequent research in a.i. has obscured the methodology of the topic. For example, the recent slew of papers on closures analysis mix implementation optimizations with specifications and leave unclear exactly what closures analysis is. In this paper, we reexamine the principles of a.i. and reformulate the topic on a foundation of coinductively defined natural semantics. We aim to demonstrate that the intensional and compositional aspects of natural semantics make it an ideal vehicle for formulating abstract interpretations of problems while preserving the essential characteristics of the subject.
Author: Yuki Komagata and David Schmidt
Writing correct programming code is necessary in computer systems development when complete testing is not possible. Intuitionistic type theory leads to a mechanical generation of correct code by using specifications. The idea is that the specification of a program is its type, and the specification can be expressed by logical formulas and proved by using mathematical axioms and inference rules of logic. Then, using the correspondence ``propositions are types'' and ``proofs are programs are values,'' a proof can be translated into correct programming code. The fundamental idea of realizability theory is that a proof can be translated into not only correct, but also minimal programming code, which contains only computational values. Based on these ideas, a realizability algorithm developed by John Hatcliff defines how a translation can be done. We analyzed Hatcliff's algorithm and implemented it in a system.
System development using specifications also leads to the idea of ``modularization.'' The cut rule of logic defines how two proofs are connected together just by looking at their specifications. This encompasses the idea of modularization and is implemented in our system.
The system is applied to the specification and proof of a modular version of insertion sort as a case study.
Author: David Schmidt
The chapter surveys the main approaches to programming language semantics, applies them to an example block-structured imperative programming language, surveys applications of semantics, and outlines areas of current research.
Author: Daniel Le Metayer and David Schmidt
A framework for static program analysis must rely on a formal semantics of the programming language to be analyzed. The best established, semantics-based, static analysis framework is abstract interpretation, whose central concept is that concrete values of the semantics of the language are replaced by abstract values that represent properties of the concrete values. In this paper, we argue that structural operational semantics (SOS) is an appropriate style for the definition of static analyses because it is both structural and intensional. Another significant quality of the SOS framework is that it can accomodate various classes of languages, and thus forms an ideal basis for the design of a program analysis platform.
Author: Allen Stoughton
Porgi is a Proof-Or-Refutation Generator for Intuitionistic propositional logic. Given a sequent, porgi either finds a minimally sized, normal natural deduction of the sequent, or it finds a "small", tree-based Kripke countermodel of the sequent. Porgi is written in Standard ML (SML/NJ Version 0.93), but generates a UNIX executable, which can be executed from the shell. See URL http://www.cis.ksu.edu/~allen/porgi.html.
Brian T. Howard
An extension of the simply-typed lambda calculus is presented which contains both well-structured inductive and coinductive types, and which also identifies a class of types for which general recursion is possible. The motivations for this work are certain natural constructions in category theory, in particular the notion of an algebraically bounded functor, due to Freyd. We propose that this is a particularly elegant core language in which to work with recursive objects, since the potential for general recursion is contained in a single operator which interacts well with the facilities for bounded iteration and coiteration.
David A. Schmidt
Two challenging but potentially fruitful research areas for programming language semantics are outlined: (i) the application of abstract interpretation as a framework for complementary language definitions for programming language design; and (ii) the use of paradigm calculi in the design of multiparadigm programming languages.
David A. Schmidt
The operational semantics of concurrent programming languages is typically coded in small-step style. Here, we adapt the abstract interpretation methodology for big-step semantics presented by the author at the 1995 Static Analysis Symposium to abstract interpretation of small-step semantics.
Recall that abstract interpretation of big-step semantics is undertaken in three stages:
An abstract interpretation methodology for small-step semantics follows the approach outlined above. The challenge to the approach comes in stage (iii), where attempts to derive a regular tree can be foiled by the ability of small-step semantics rules to generate new source program syntax on the fly, which can happen, for example, in the semantics of a concurrent program that spawns new processes. Techniques to limit---indeed, to abstractly interpret---program syntax generation are presented. Several example languages are presented: a while-loop language with parallelism; a subset of CCS; and a subset of the pi-calculus.
David A. Schmidt
Based upon previous work on abstract interpretation of programs with a big-step operational semantics, a technique is derived for abstract interpretation of programs with a small-step semantics. A distinguishing feature of small-step semantics is the generation of new program syntax during the calculation of a program's semantics. (This can happen when a concurrent program spawns new processes, for example.) This complicates convergence checking of an abstract interpretation. Techniques to limit---indeed, to abstractly interpret---program syntax generation are presented and applied to several example languages: a while-loop language with parallelism, a subset of CCS, and a subset of the pi-calculus.