A key area of foundational research for the project has been the
formalization of data-flow analysis of ML-like programs in
Detailed Summary of Technical
Progress.
-
Languages and Tools for Verified, Modular Programming
-
Lemon: A Functional Language with Inductive and Coinductive Types.
The functional language lemon is based on the simply-typed lambda
calculus augmented with sums, products, and the mu and nu constructors
for least (inductive) and greatest (coinductive) solutions to recursive
type equations. The term constructors of the language strictly follow
the introduction and elimination rules for the corresponding types; in
particular, the elimination for mu is iteration and the introduction
for nu is coiteration (also called generation). Version 1.2, an
interpreter implemented in Standard ML, is available for ftp, along
with a collection of programming examples.
-
Implementation of Intuitionistic Type Theory and Realizability Theory.
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.
-
porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional
logic.
Given an intuitionistic propositional logic sequent,
Gamma |- phi, porgi either finds a minimally sized, normal
natural deduction of phi from the assumptions in Gamma, or it
finds a finite, tree-based Kripke model whose root node forces all of
the formulas in Gamma but does not force phi. Although an
attempt is made to minimize the size of the Kripke countermodels, such
countermodels are not always minimally sized. On the other hand:
-
These models never have redundant nodes, i.e., it is never
possible to reduce the size of one of porgi's countermodels simply by
deleting certain nodes.
-
Classical models are produced whenever possible. Thus, if a model
with more than one node is produced, one can conclude that the sequent
is provable classically.
-
In porgi's countermodels, child nodes always force strictly more
subformulas of the original sequent than do their parents.
Porgi can also handle minimal logic, is capable of generating typed
lambda terms instead of natural deductions, and can display the
subformulas of a sequent that are forced at each node of a Kripke
countermodel.
-
Foundational research on program analysis
-
Natural-Semantics-Based Abstract Interpretation.
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.
-
Systematic Programming with Induction and Coinduction: A Case Study.
In ``A Synthesis of Several Sorting Algorithms'', 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 the structure of each
algorithm.
Transitions and DOD Interactions.
Software and Hardware Prototypes.
-
Lemon: A testbed interpreter for a functional language with inductive
and coinductive types, where the control structures strictly follow the
type structures.
Documentation and implementation available from
http://www.cis.ksu.edu/~bhoward/lemon.html.
-
A realizability system for generating ML-like programs.
Documentation and implementation available from
ftp://ftp.cis.ksu.edu/pub/CIS/Students/realizer/
-
porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional logic.
Documentation and implementation available from
http://www.cis.ksu.edu/~allen/porgi.html.
List of Publications.
- Banerjee, A., and Schmidt, D.A.
Stackability in the typed call-by-value lambda calculus.
Science of Computer Programming, in press.
- Howard, B.T.
Inductive, coinductive, and pointed types.
Proc. 1996 ACM SIGPLAN International Conference on Functional Programming,
in press.
- Howard, B.T.
Another iteration on Darlington's ``A synthesis of several sorting
algorithms''.
Acta Informatica, to appear.
- Le Metayer, D., and Schmidt, D.A.
Operational and denotational semantics.
ACM Computing Surveys, in press.
- Le Metayer, D., and Schmidt, D.A.
Structural Operational Semantics as a Basis for Static Program Analysis.
ACM Computing Surveys, in press.
- Schmidt, D.A.
Operational and Denotational Semantics.
ACM Computing Surveys, in press.
- Schmidt, D.A.
Programming language semantics.
In
CRC Handbook of Computer Science,
Allen Tucker, ed.,
CRC Press, Boca Raton, FL, in press.
- Schmidt, D.A.
Natural-semantics-based abstract interpretation.
Proc. 2d Static Analysis Symposium, Glasgow.
Lecture Notes in Computer Science 983, Springer, Berlin, 1995, pp. 1-18.
- Stoughton, A.
porgi: A Proof-Or-Refutation Generator for
Intuitionistic propositional logic, submitted to CADE-13.
Invited and Contributed
Presentations.
- D. Schmidt. Coinductively defined natural semantics.
University of Edinburgh, August 1995, and University of Copenhagen, August
1995.
- D. Schmidt. Linear logic and single threading.
Workshop on Syntactic Control of Interference and Linear logic,
Glasgow, August 1995.
- D. Schmidt.
Natural-semantics-based abstract interpretation.
Keynote speaker, Proc. 2d Static Analysis Symposium, Glasgow, September, 1995.
-
A. Stoughton, "Equationally fully abstract models of PCF", Workshop on
the Full Abstraction Problem for PCF and Related Langauges, Aarhus
University, Denmark, April 1995.
-
A. Stoughton, "Mechanizing logical relations", Workshop on
the Full Abstraction Problem for PCF and Related Langauges, Aarhus
University, Denmark, April 1995.
-
A. Stoughton, "Studying the fully abstract model of PCF within its
continuous function model", Workshop on the Full Abstraction Problem
for PCF and Related Langauges, Aarhus University, Denmark, April 1995.
Honors, Prizes or Awards
Received.
- D. Schmidt. Funded visiting research fellow, Computing Science Department,
University of Glasgow Research Festival, July-August 1995.
- D. Schmidt. Invited participant, Dagstuhl Workshop on
Abstract Interpretation, Dagstuhl, Germany, August 1995.
- D. Schmidt. Funded visitor, Computer Science Department,
University of Copenhagen, August 1995.
- D. Schmidt. Invited keynote speaker,
Proc. 2d Static Analysis Symposium, Glasgow, September, 1995.
- D. Schmidt. Invited participant, Dagstuhl Workshop on
Multiparadigm Languages, Dagstuhl, Germany, September 1995. (Declined
invitation due to time constraints.)
- D. Schmidt and A. Stoughton. Co-principal investigators,
National Science Foundation Grant CCR-9302962,
Analysis and Classification of Programming Languages,
September 1993-January 1997, $221,000. (The 1995 allocation was $73,000.)
-
A. Stoughton. Funded invited participant and speaker, Workshop on the
Full Abstraction Problem for PCF and Related Languages, Aarhus
University, Denmark, April 1995.
-
A. Stoughton. Invited participant, Program on Semantics of
Computation, Newton Institute of Mathematical Sciences, Cambridge
University, 6-30 July 1995.
Service to Profession.
- D. Schmidt.
Program Committee Member, ACM Symposium on Partial Evaluation
and Semantics-Based Program Manipulation,
La Jolla, CA, June 1995.
- D. Schmidt.
Program Committee Co-Chair,3rd International Symposium on Static
Analysis, Aachen Germany, to be held in September 1996.
- D. Schmidt.
Program Committee Member,2d Andrei Ershov Second International Memorial Conference:
Perspectives of System Informatics.
Novosibirsk, Russia, to be held in June 1996.
- D. Schmidt.
Guest Editor, with Michael Mislove,
Proceedings of the Tenth Workshop on the Mathematical Foundations of
Programming Semantics,
Theoretical Computer Science, to appear.
Project Personnel Promotions.
Project Staff.
- Name: Dr. David A. Schmidt
- Name: Dr. Allen Stoughton
- Name: Dr. Brian T. Howard
Multimedia URL.
- EOYL
FY95
- QUAD
FY95
Keywords.
- Type theory.
- Intuitionistic Logic.
- Abstract interpretation.
Business Office