Mathematics and Computation

A blog about mathematics for computers

A modular formalization of type theory in Coq

Here are the slides for the talk I just gave at TYPES 2017 in Budapest. It is joint work with Philipp Haselwarter and Théo Winterhalter. The abstract for the talk is available online.

It describes a complete formalization of dependent type theory which allows you to turn various features of type theory on and off, and it proves several basic formal theorems.

GitHub repository: formal-type-theory
Slides: TYPES 2017  – A modular formalization of type theory in Coq [PDF]


Your abstract says you prove uniqueness of typing. How do you prove that? IME to show this, you have to have the injectivity of judgmental equality at pi-types, and I've only ever been able to establish this via an argument involving logical relations. Is there some easier technique I've missed?

I am not sure I understand you. Are you saying that you expect $\prod_A B \equiv \prod_C D$ to imply $A \equiv C$ and $B \equiv D$? To be honest, I just started typing it up in Coq and then Coq wanted me to invent a more general induction hypothesis, and I did. The usual stuff. Let me put some comments into the relevant file and come back to you.

Oh, perhaps it's worth mentioning that the syntax is fully annotated. In particular, abstractions are written as $\lambda A . B . e$ and applications as $e_1 @^{A.B} e_2$, indicating both the domain and the codomain. Is that what worries you?

We're currently in the process of modifying syntax so that it becomes configurable. Then it should be clearer what assumptions precisely are needed for uniqueness.

Hi Andrej,

You have indeed understood what I meant.

If you try to prove that typing is unique up to judgmental equality for the usual syntax, you run into a problem in the application case. Induction tells you that ?AB??CD, but you can't conclude that A?C and B?D from that, which is what you need to get the proof to go through.

Adding annotations to applications and lambdas should fix this problem (and since you did it in Coq, it obviously does fix it). I didn't read your Coq development closely enough to realize that this is what you were doing, but your explanation makes things make sense to me now.

Andreas Abel

Injectivity of Pi-types usually requires a logical relation argument. See Abel/Scherer, LMCS 2012.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention, I will gladly respond. You are also welcome to contact me directly.