In a proof checker, we are interested in proofs; no other evidence for a judgement is acceptable. There is a question, however, whether we insist on objects that are immediately recognisable as proofs, or will accept some meta-notations that only compute to proofs. For example the deduction theorem is a sound rule (e.g. admissible) of Hilbert style minimal implicational logic, because a proof of G|-a->b can be computed from a proof of G,a|-b, but it is not directly a rule of the logic. Even if we allow a proof checker to directly implement such rules, we cannot expect to know and implement all the sound rules users may want. This talk is about how to construct a proof checker such that the stringent requirement of formality can be met without sacrificing the convenience and computational efficiency of such indirect proof notations as admissible rules.

Isn't this just what LCF tactics are for? Surprisingly, although LCF tactics are programmed in a Turing-complete programming language (e.g. SML), only derivable rules are representable. Further, because SML's type system is not expressive enough to specify which theorem a tactic will return, and because SML has general recursion which may not terminate, tactics must actually be evaluated, which is infeasible for many rules.

My proposal is to program LCF-style proof checkers in languages with only terminating functions, and dependent type systems. Then many non-derivable rules can be expressed as tactics, and these tactics for admissible rules can be used without being executed, because they cannot fail to terminate if executed, and their type tells explicitly which theorem they will return.

A paper about this work is available here.