Scottish Theorem Provers Seminar

Friday, 11th September, 1998

11am-5pm

Room CG83, Chemistry/Geology Building,

Science Site, Stockton Road,

Durham

Hosted by the Reasoning Group of the Computer Science Department at the University of Durham.

Programme

11:00-11.30	Arrival and Coffee
11.30-11.40	Welcome
11:40-12:20	Proof Checking + Model Checking = LegoMC	Shenwei Yu, Durham
12.20-13.00	Permutation-free calculi for proof search in some constructive logics	Roy Dyckhoff, University of St. Andrews
13:00-14:15	Lunch
14:15-14:55	Lightweight Formal Methods for Computer Algebra Systems	Martin Dunstan, St. Andrews
14:55-15:35	Dependently Typed Functional Programming in LEGO	Conor McBride, Edinburgh
15:35-16:00	Tea
16:00-16:40	The type of the empty (search) tree	James McKinna, Durham
16:40	Close

Abstracts

Permutation-free calculi for proof search in some constructive logics

Roy Dyckhoff, St. Andrews

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.)

Dependently Typed Functional Programming in LEGO

Conor McBride, Edinburgh

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

Shenwei Yu, Durham

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.

Lightweight Formal Methods for Computer Algebra Systems

Martin Dunstan, St. Andrews

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.

The type of the empty (search) tree

James McKinna, Durham

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.