Benjamin Werner explore a type theory that, among other things, might be a first step towards making a proof assistant that's also a more traditional programming environment in On the Strength of Proof-Irrelevant Type Theories, Logical Methods In Computing 2008.

Abstract. We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. Finally we describe a simple set-theoretic semantics.

A suggested application lies a few paragraphs in.

In order to identify more terms it thus is tempting to [integrate] program extraction into the formalism so that the conversion rule does not require the computationally irrelevant parts of terms to be convertible.

In what follows, we present and argue in favor of a type-theory along this line. More precisely, we claim that such a feature is useful in at least two respects. For one, it gives a more comfortable type theory, especially in the way it handles equality. Furthermore it is a good starting point to build a platform for programming with dependent types, that is to use the theorem prover also as a programming environment. ...

## Recent comments

3 hours 34 min ago

5 hours 21 min ago

6 hours 28 min ago

8 hours 35 min ago

12 hours 47 min ago

1 day 1 hour ago

1 day 1 hour ago

1 day 1 hour ago

1 day 9 hours ago

1 day 9 hours ago