13
$\begingroup$

There's:

https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf

And a few other books, but they don't detail how one goes about implementing say another Lean, Coq, or Isabelle. How did the original authors of those software figure out how to implement things?

Where's that book?

Also, there's all of these: http://freecomputerbooks.com/mathLogicBooks.html

But you can't expect me to search through every book in search of how to implement things. So was wondering if anyone here already knows what book to pick.

$\endgroup$
  • $\begingroup$ Found this: ropas.snu.ac.kr/~kwang/520/pierce_book.pdf $\endgroup$ – AbstractAlgebraLearner Dec 7 '19 at 15:57
  • 3
    $\begingroup$ I think implementation of something like Coq is research-level work in type theory and the theory of programming languages. There are certainly textbooks on the theory of programming languages, but I think the answer to how the designers of your examples knew how to do this is that they were longtime experts in the subject. $\endgroup$ – Kevin Arlin Dec 7 '19 at 17:37
  • $\begingroup$ Or they had tried, learned what didn't work, and tried again — see both dead proof assistants (Alf, Lego, a million more), and early versions of the ones that were rewritten (at least Lean, maybe Agda 1?). $\endgroup$ – Blaisorblade Dec 15 '19 at 15:03
24
$\begingroup$

There is no such book. If someone wants to implement a proof assistant based on type theory now, they can look at a) tutorial implementations b) papers c) source code of existing systems.

The issue with a) is that it only covers a small fraction of real-world functionality and commonly presents naive solutions which don't scale and differ greatly from real-world implementation. The issue with b) is that it's scattered, contains lots of outdated and irrelevant information, requires expertise to navigate, and it's also incomplete with respect to real-world systems. The issue with c) is that it's even harder to navigate and contains many legacy hacks and suboptimal solutions.

It is also the case that the core implementations of the real-world systems are very different. E.g. Coq elaborates induction to fixpoints and case splits, Agda to recursive definitions and case trees and Lean to eliminators. There is also no clear consensus on design philosophy and in particular on how big a "kernel" should be and what it should include.

Nonetheless, I can do a quick survey on references. Be warned that it is highly opinionated and reflects my personal take on the subject.

1. Basic type checking and conversion checking

A modern view on this matter is that Coquand's semantic type checking algorithm is the preferred basic algorithm because of its performance and simplicity. Bidirectional type checking is another ubiquitous foundational principle. All of the sources below use both.

2. Basic unification and inference

Here, the core ideas used in the larger systems are pattern unification and contextual metavariables. See my introduction.

3. Advanced unification, elaboration, implicit arguments

  • Chapter 3 of Ulf Norell's thesis is good introduction to implicit arguments and constraint postponing. I have again a small implementation for implicit arguments (not for postponing though).
  • Abel & Pientka on advanced unification features, most of which are implemented in Agda. This is a bit dense and short on implementation details.
  • Gundry & McBride significantly overlaps with the previous reference, and is helpful as an alternative take.
  • Ziliani & Sozeau on unification. Describes a version which is not the one actually implemented in Coq, but which is fairly close. Contains many implementation-relevant details.

4. Inductive types, induction, termination checking

At this point, approaches diverge and literature becomes sparse. Coq, Agda and Lean have greatly different implementations.

  • Mini-TT has simple inductive types and dependent case splits. Less expressive than Coq/Agda but good as starting point.
  • Reference on the calculus of inductive constructions used in Coq. This is fairly detailed, and it should be possible to do an implementation based on this.
  • The most recent piece on Agda pattern matching. Also partly describes inductive types in Agda. Fairly technical.
  • The third main approach is compiling to eliminators, which is used in Lean AFAIK. The Lean elaboration paper lists references on elaborating to eliminators.

On termination checking, the main reference is this, which is very similar to the one used in Agda. I'm not familiar with the Coq termination checker, I believe the basic principles are the same, although the Agda one is more powerful/complicated. In Lean, termination checking is implicit in the compilation to eliminators.

5. Modules, type classes, automation

Unfortunately, I run out of expertise at this point, and I'm not sure what are the good references and approaches. The CiC manual and Norell's thesis can be used to copy the Coq or Agda module implementation. For tactics, reflection and type classes, I imagine the best would be to dig into Coq/Agda/Idris/Lean docs and sources and learn how they work.


I haven't mentioned Idris so far, because it's similar to Agda, and its unique features are fairly experimental and more relevant to programming than to proof writing. I'm mentioning error reflection here specifically which I think is highly useful in any system.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.