Friday, 11th September, 1998
Room CG83, Chemistry/Geology Building,
Science Site, Stockton Road,
Hosted by the Reasoning
Group of the Computer
Science Department at the University of Durham.
Derivations in a (cut-free) Gentzen calculus such as LJ are
interpretable as (normal) natural deductions, but the
interpretation, although onto, is many-one, because of the
permutability of inference rules in the Gentzen
calculus. This leads to undesired redundancy in the use of
the calculus as a tool for proof search. In this talk we
discuss the use of 'permutation-free' calculi, arising from
work of Herbelin, for proof search in logics such as
intuitionistic logic and lax logic: in particular, we
present such a calculus for proof search in a version (the
LF) of Martin-Lof type theory. (Joint work with Jacob Howe & Luis Pinto.)
I shall discuss my recent work adding dependently-typed
functional programming facilities to LEGO. Functional
programs become LEGO terms involving the usual elimination
rules provided for inductive datatypes. The equational
problems arising from the elimination of constrained
inductive families are solved automatically in first-order
constructor-form cases, given the additional axiom that
identity proofs are unique.
By way of example, I shall exhibit a dependently typed
functional program which implements first-order unification
solely by structural recursion, recently compiled into LEGO
and proven correct.
Proof Checking + Model Checking = LegoMC
Interactive theorem proving usually involves many tedious and trivial
proving steps. Certain amount of automation can release people from
those irrelevant details so that they can focus on issues which are
really concerned. Our method is to adapt existing algorithms to generate
proof terms automatically. Those proof terms can then be integrated with
other proof terms generated by other automatic algorithms or interactive
theorem provers to complete the whole proof. On the other hand, type
checking of proof terms can further ensure the correctness of proofs
generated by automatic algorithms. We have implemented a model checker,
LegoMC, for automatic verification of finite systems.
This talk will be about the use of lightweight formal methods to improve
the reliability of computer algebra systems. In particular we are looking
at the use of the Larch two-tiered specification system applied to Aldor
and the strongly-typed AXIOM computer algebra system. Our motivation is
that the algorithms used in these systems have been well studied and that
they do behave as expected. We believe that it is more likely that any
unexpected behaviour (wrong answers) will be the result of applying such
routines in circumstances for which they were not designed. More subtle
problems may arise in AXIOM when the behaviour of the computer algebra
domains and categories does not quite coincide with the documentation.
Type theories of various kinds have long held out the
possibility of being used as a basis for (functional)
programming, but their use so far has largely been confined
to specification and proof, via propositions-as-types.
But we may also exploit type dependency in programming, for
example in Augustsson's Cayenne system, and in this talk I
want to focus on the use of dependent types to analyse
binary search trees.
A tension exists between exploiting type dependency, while
excluding (possibly undecidable) propositions from our
programming language. One recent proposal of Luo is to
forbid empty types from the language, which leads to
unexpected types for the empty search tree.
This is work in progress.