PRL Seminars

Many investigators have considered the possibility of extracting programs in a functional language from natural deduction proofs in intuitionistic logic. This approach delivers programs littered with redundant components and has led people to examine various ways of pruning these useless subprograms.

Here we give an algorithm for automatically performing this pruning without requiring the user to manually annotate the whole proof. It then becomes possible to allow classical reasoning at points in the proof whose putative computational content is redundant to the extracted program. One particularly good place to take advantage of this new ability is in a rule for well-founded induction which allows us to extract explicitly recursive programs.

Unfortunately, all this new flexibility leads to a complication which has not been mentioned in the literature: by pruning supposedly redundant parts of the extracted program we destroy the subject reduction and strong normalization properties that are touted as one of the main advantages of the programs-from-proofs approach.

The main original result of this work is a propositional type system which inserts a relatively small number of "delay" and "force" operators to restore these properties. We attempt to extend the result to a dependent type system based on first-order predicate logic via the erasure of dependent types.