7
$\begingroup$

There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (implementing, not using) proof assistants, because they introduce only the core mechanics, and so they are much easier to comprehend.

Are there similar projects out there featuring an extensional equality type? I would like to see some general principles when dealing with extensional equality types.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ I don't think it's a tutorial, but would Andromeda fit the bill? (There are also some implementations of PRL that might be sufficiently tutorial-style/lightweight, but this implementation strategy is very different and I wasn't sure what you were looking for.) Regarding general principles, I think the jury is still out --- but I find the ideas discussed in Andromeda to be interesting and pertinent. $\endgroup$
    – Jonathan Sterling
    Apr 18, 2022 at 6:35
  • 1
    $\begingroup$ Andromeda is in a rather sorry state at the moment, it needs to be cleaned up. I've got some ideas on what to do after I am done organizing ICFP 2022. But you could contact Philipp Haselwarter and Anja Petković if you'd like to know more about it. $\endgroup$
    – Andrej Bauer
    Apr 18, 2022 at 7:29

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.