Bib::flatau92
A. D. Flatau A verified implementation of an applicative language
with dynamic storage allocation
(ftp://ftp.cs.utexas.edu/pub/boyer/diss/flatau.pdf), University of Texas
at Austin, Ph.D. dissertation, 1992 (minus some appendices).
Relevance: a second verified compiler hosted on
the CLI Verified Stack
———
Abstract
A compiler for a subset of the Nqthm logic and a mechanically checked
proof of its correctness is described. The Nqthm logic defines an
applicative programming language very similar to McCarthy's pure Lisp [20].
The compiler compiles programs in the Nqthm logic into the Piton assembly
level language [23]. The correctness of the compiler is proven by showing
that the result of executing the Piton code is the same as produced by the
Nqthm interpreter V&C$. The Nqthm logic defines several different
abstract data types, or shells, as they are called in Nqthm. The user can
also define additional shells. The definition of a shell includes the
definition of a constructor function that returns new objects with the type
of that shell. These objects can become garbage, so the run-time system of
the compiler includes a garbage collector. The proof of the correctness of
the compiler has not been entirely mechanically checked. A plan for
completing the proof is described.
———
The version of the compiler presented in the dissertation included code
for creating new shells and a garbage collector. But these features of the
compiler were not fully verified at the time the dissertation was defended.
An earlier version of the compiler dealt only with the Nqthm primitives
CAR, CDR, CONS, FALSE, LISTP, NLISTP,
TRUE, TRUEP, and IF, as well as recursive functions. The
run-time of that simpler system included dynamic storage allocation (to
allocate conses in Piton's array space). But it did not include a garbage
collector. It was that simpler implementation that was mechanically
verified. The completion of the proofs of the full system was never
completed.
The Nqthm events for this work may be found in the *.events files
of examples/flatau/.
