|
This thesis contributes to the construction of a convenient specification
language on top of a type theoretic substrate. The subject arose in the
context of the Typelab project that aimed at
improving the machine assistance for the formal development of mathematics,
software and hardware. Type theory was chosen as underlying theoretical
framework, because it homogeneously comprises both the notion of computation
and deduction. However, the price for its expressiveness is a verbose
syntax. When I joined the Typelab group, my responsibility was to shape the
external language of the Typelab system. Naturally, I first looked at
related implementations. Most of them cope with the wordiness of type
theory by allowing their users to omit on input redundant parts that can be
inferred automatically through a process called elaboration. While the use
of such a mechanism seems indispensable for serious verification tasks, I
found the existing solutions unsatisfactory. Not only are the implemented
algorithms seldom precisely documented and formally analyzed, they also lack
strength. It is disappointing how much redundant information still has to
be supplied on input. Furthermore, the ad hoc erasure algorithms, used to
reduce the redundancy of expressions on output, often produce wordy or even
ambiguous external representations. Such failures are especially fatal for
interactive verification systems, where the output describing the actual
system state is often the only hint for a user on how to proceed with a
proof. To improve this situation, I developed the elaboration and erasure
methods described in this thesis.
The design of elaboration is inspired by the conciseness of functional
programming languages and is formally grounded on type inference in the
underlying type theory. To establish correctness, intermediate elaboration
states are represented by open terms, adapting techniques recently developed
for the representation of partial proofs. The erasure methods are based on
estimations of the corresponding elaboration process and guarantee a
successful reconstruction of the elided information. Experiments performed
with Typelab proved the proposed methods both effective and efficient.
| |