# Typing proof trees or proof objects

Is there a theory of typing proof objects or proof trees?

Partially inspired by this question and answer, I was wondering about separating type checking into two phases: the first phase infers a full proof tree and the second phase checks if the proof tree is well formed and conclusions follow from premises.

Potentially, this sort of separation allows a smaller kernel. Also the kernel can be written as a total function within a prover of similar power without extra axioms. I think it's the driver which infers the proof trees which would require extra axioms.

What I mean is you can provide explicit witnesses for typing judgements.

For the STLC, something like this:

$$\frac{\begin{split} q_0 \colon [ \Gamma \vdash e_0 \colon \tau_0 \rightarrow \tau_1 ] \\ q_1 \colon [ \Gamma \vdash e_1 \colon \tau_0 ] \end{split}}{ q_0 q_1 \colon [ \Gamma \vdash e_0 e_1 \colon \tau_1 ] }$$

$$\frac{q \colon [ \Gamma , x \colon \tau_0 \vdash e \colon \tau_1 ]}{ \lambda x \colon \tau_0. q \colon [ \Gamma \vdash \lambda x \colon \tau_0 . e \colon \tau_0 \rightarrow \tau_1 ] }$$

$$\frac{x \colon \tau \in \Gamma}{ x \colon \tau \in \Gamma \colon [ \Gamma \vdash x \colon \tau ] }$$

The meat and potatoes is when you have more complicated features like dependent types. You'd want explicit witnesses for judgemental equalities something like:

$$\frac{\begin{split}q \colon [ \Gamma , x \colon \tau \vdash e \colon \tau' ] \\ q' \colon [ \Gamma \vdash \colon e' \colon \tau ]\end{split}}{\beta(x \colon \tau \mathrel{:=} q' , q) \colon [ \Gamma \vdash (\lambda x\colon \tau. e) e' \triangleright_\beta [x \mathrel{:=} e'] e ]}$$

$$\frac{\begin{split} q \colon [\Gamma \vdash \tau \equiv \tau'] \\ q' \colon [\Gamma \vdash e \colon \tau] \end{split} }{ \textbf{J}(q, q') \colon [ \Gamma \vdash e \colon \tau' ]}$$

Anyhow, it quickly gets very redundant, confusing and unreadable.

I'm confused about several aspects of this.

1. You want proof trees to be trivial to check but you also want them to not be redundant. What should it mean for it to be "trivial" to infer a property of the root of the proof tree like the environment or type?

2. It's really confusing to notate proof trees. Is there a better way of writing this silliness?

3. Are there existing references or work in this direction?

4. It's hard to come up with a reasonable meaning for proof trees. I guess you can see them as terms annotated with explicit environments and types?

What you are describing already happens to a large extent in a proof assistant with a trusted kernel.

Side remark: I prefer to say "derivation" instead of "proof tree" because derivations need not be about proofs, they can also be about constructions.

User input typically requires elaboration to a more explicitly annotated type theory (the process of elaboration is intertwined with the process of type-checking), let us call it the core type theory. The core type theory is designed in such a way that the judgements already encode the proof trees, except for judgemental equalities.

For example, in the simply-typed $$\lambda$$-calculus with explicitly annotated types of variables ($$\lambda (x : A) . e$$ instead of just $$\lambda x . e$$), the derivation of $$\Gamma \vdash e : A$$ can be read off immediately from $$e$$. There is no point in storing any extra information anywhere, as it is all there already. One only has to process $$e$$ to either reconstruct the derivation or decide that $$e$$ does not encode a valid one. This is the meaning of “terms as proofs”.

Proofs of judgemental equalities are typically not recorded for two reasons:

• They are proof irrelevant: it does not matter which proof is provided, as long as there is one. Consequently, if we have the means to reconstruct them when they exist, we need not store them.

• It is often deemed that derivations of judgemental equalities are too large to be stored. Instead, the core type theory is designed to have decidable equality checking so that the missing derivations can be reconstructed algorithmically. In a sense we are storing the derivations in time rather than in space.