Type system metatheory formalization in Lean 4

Stream: Program verification

[Danila Danko]

Hi!

I'm new to Lean and formal verification in general. Recently, I started studying publications about type systems and noticed that some authors, e.g., [1],[2],[3], provided proofs of various properties of metatheory of their type systems, e.g., soundness and completeness of the algorithmic system w.r.t. the declarative system, and the decidability of the type inference algorithm in that system.

I thought it was cool that it was possible to mechanize results about type systems. Hence, I decided to search for resources that could teach me how to prove properties about metatheory of programming languages, e.g., to be able to prove things about the type system in [1] or [4] myself.

Most authors used hand-written proofs, Agda, or Coq. I learned that [3] used Lean 4 for proofs, and the proofs took 16KLOC (https://proofassistants.stackexchange.com/a/2506). This amount of code would be quite overwhelming to study.

Then, I found https://github.com/rami3l/PLFaLean. It provided a chapter about bidirectional type checking, but there seemed to be no info about extrinsic typing, unification and mutable cells in metavariables, techniques used in [4] and GHC.

So, my questions:

1. What kind of metatheory is Lean convenient to use for?
2. Which (digestible) works use Lean 4 for proofs about metatheory?
3. How do you prove correctness and completeness of bidirectional typing algorithms like in [1] or [4]? Which proof assistant would you choose for this task and why?

References
[1] J. Dunfield and N. R. Krishnaswami, “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism,” Aug. 22, 2020, arXiv: arXiv:1306.6032. doi: 10.48550/arXiv.1306.6032.
[2] S. Jiang, C. Cui, and B. C. D. S. Oliveira, “Bidirectional Higher-Rank Polymorphism with Intersection and Union Types,” Proc. ACM Program. Lang., vol. 9, no. POPL, pp. 2118–2148, Jan. 2025, doi: 10.1145/3704907.
[3] J. E. Ghalayini and N. Krishnaswami, “Explicit Refinement Types,” Proc. ACM Program. Lang., vol. 7, no. ICFP, p. 195:187-195:214, Aug. 2023, doi: 10.1145/3607837.
[4] S. P. Jones, D. Vytiniotis, S. Weirich, and M. Shields, “Practical type inference for arbitrary-rank types,” J. Funct. Prog., vol. 17, no. 1, pp. 1–82, Jan. 2007, doi: 10.1017/S0956796806006034.

[Bas Spitters]

A canonical introduction is https://softwarefoundations.cis.upenn.edu/ (in Rocq).
There's a Lean port (https://alashworth.github.io/sf-lean/index.html), but I don't know what the status is.
This one is also recommended: https://lean-forward.github.io/hitchhikers-guide/2023/

[Danila Danko]

@Bas Spitters thanks! On the PLF Postscript page, I found a link to http://iron.ouroborus.net/ and there a link to https://github.com/discus-lang/iron/.

Iron Lambda is a collection of ​Coq formalisations for functional languages of increasing complexity.

Looks digestible, although it's in Rocq.

[Jannis Limperg]

A student of mine recently formalised a standard Martin-Löf type theory in Lean. (Code is not public yet.) Using Lean (as opposed to Rocq or Agda) was fine except for the issue discussed here: rule induction over mutually inductive predicates is unsupported. Depending on your theory, this issue might be really annoying, or it might not matter at all.

[Danila Danko]

@Jannis Limperg did your student use an intrinsically typed representation?

I'm curious because PLFA argued for intrinsic typing (Section 5) and there was a discussion regarding the preferred approach: https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/Intrinsic.20or.20Extrinsic.20Typing.20for.20PL.20Metatheory.3F/with/472052866

[Jannis Limperg]

No. He (@Johannes Reichle) used intrinsically scoped syntax, i.e. terms are annotated with the number of free variables in them, but not intrinsically typed syntax. Since this is a full dependent type theory, I'm not sure whether intrinsic typing would be practical (possible?) without induction-recursion.

Personally, I'm also a big hater of intrinsic typing. I feel like it adds a ton of complexity as soon as you have any sort of dependency structure. For simple theories, it is pretty, though.

[Bas Spitters]

@Danila Danko You mean also want to have a look at the POPLmark and POPLmark Reloaded benchmarks: https://poplmark-reloaded.github.io/
Hint: Lean4 is still missing ;-)

[Danila Danko]

@Bas Spitters thanks!

• Both benchmarks have accompanying PDFs that provide context about tasks.
• Some of the solutions, especially for the non-Reloaded POPLMark problems, have extensive explanations.
• The Coq proofs in the POPLmark Reloaded version are relatively small and readable.
• Implementing a Lean 4 version is a good challenge :) I couldn't find implementations on GitHub.

[Chris Henson]

@Danila Danko I recently made this blog post "Beginner Resources for Formalizing Lambda Calculi" that has a couple of projects you've not already mentioned: https://chrishenson.net/posts/2025-05-10-formalized_lambda_calculus.html

It includes a link to my own repo in Lean 4 that currently just has a proof of beta confluence for simple types with pairs.

[Danila Danko]

@Chris Henson thanks! The resources on formalization aren't that scarce!