Joshua Grosso (Jun 22 2021 at 22:51): Joshua Grosso (Jun 22 2021 at 22:51):I fear these questions might be too broad to be answerable, but I'll try just in case. If it helps at all, I'm a CS undergraduate student in the US (namely, a rising senior hoping for grad school).
My impression is that formal verification is still in the relatively early stages of development as a field. To be clear, I don't mean this pejoratively at all—it means there's a place for ugrads like me to contribute :-) Along these lines, I'm currently working on a research project to formalize TAPL after where Software Foundations leaves off (or, at least, as much as possible before I graduate). But, I'm a bit worried because it's a rather limited endeavor—my university is really small and so it's just my faculty mentor and me. We've been learning how to practically use Coq on-the-fly... and in my case, I've been learning type theory as I go.
Given that TAPL is an introduction to type theory, is a project like this too trivial to be "interesting"—especially if we aren't able to make all the way through the later chapters?
Furthermore, some of TAPL has been covered many times over by (for example) existing solutions to the POPLmark challenge. Would an extra formalization of such material be little more than noise at this point in the grand scheme of things? Or is the corpus of formally-verified material still small enough that this isn't a major concern?
Martin Harrison (Jun 23 2021 at 09:40):You can be assured that most of your work at this stage of life will be noise, and I don't mean this pejoratively at all. You have an idea, you want to execute and you even have a partner to help - go for it! I'll even help you if you decide to put in on GitHub.
Joshua Grosso (Jun 23 2021 at 21:53):@Martin Harrison Thanks for the advice, I'll ask my advisor about making it public when I meet with him next week!
Matthieu Sozeau (Jun 25 2021 at 08:47):I guess B. C. Pierce wouldn't mind to add a link to formalizations of TAPL lemmas if they existed :)
Xuanrui Qi (Jun 29 2021 at 17:50):Formalizing H-M type inference would be a particularly interesting exercise, and not trivial at all.
Joshua Grosso (Jun 29 2021 at 18:01):Xuanrui Qi said:
Formalizing H-M type inference would be a particularly interesting exercise, and not trivial at all.
It's funny that you mention that, since I'm currently working on formalizing Chapter 22: Type Reconstruction, which is type inference for STLC (although I assume H-M would be a lot more difficult). Apparently though, another team beat me to it last year: https://seer.ufrgs.br/rita/article/view/Vol27_nr3_13/pdf_1
Ben Siraphob (Jul 02 2021 at 17:08):@Joshua Grosso I am also an undergraduate in the US (rising junior in CS and math), let me know if you decide to tackle this, since I've also been on the lookout for more-than-toy projects beyond the Programming Langauge Foundations volume of Software Foundations.
Joshua Grosso (Jul 02 2021 at 21:25):Hi! I don't currently plan on formalizing H-M type inference proper, only what TAPL covers in "Type Reconstruction" (which takes place before the material on polymorphism).
Emilio Jesús Gallego Arias (Jul 02 2021 at 22:51):that's a very interesting topic and indeed there are very interesting and different approaches to attack such a problem
Emilio Jesús Gallego Arias (Jul 02 2021 at 22:52):my fav so far would be based off Gonthier's solution to POPL Mark + small inversions
Matthieu Sozeau (Jul 05 2021 at 07:19):There's a paper by Affeldt IIRC that tackles HM(X) even handling GADTs
Xuanrui Qi (Jul 26 2021 at 07:32):IIRC there's something about HM(X). The other thing I know is "A Certified Implementation of ML with Structural Polymorphism and Recursive Types", and we're currently working on an extension of it with GADTs. However, there are some difficulties
Jacques Garrigue (Jul 27 2021 at 06:55):I'm curious of the one about HM(X). Definitely, it is not by Affeldt, and I couldn't find it online.
The original references for Hindley-Milner in Coq and Isabelle are:
C. Dubois and V. Ménissier-Morain. Certification of a type inference tool for ML: Damas-Milner within Coq. Journal of Automated Reasoning, 23(3):319–346, Nov. 1999.
W. Naraschewski and T. Nipkow. Type inference verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning, 23:299–318, 1999.
I do have a ssreflect version of unification too, just to show that one does not really need automation.
http://www.math.nagoya-u.ac.jp/~garrigue/papers/unification/ssrunify.v
(Sorry for the unreadable comments. They are in Japanese.)
Joshua Grosso (Aug 14 2021 at 22:20):As part of my research project, I've taken a shot at formalizing Functional Pearls: ⍺-conversion is easy (Altenkirch, 2002). It's still a work-in-progress, but (I think) I've been able to formalize the main results! In case anyone finds it interesting, I've uploaded it to github.com/jgrosso/coq-alpha-pearl. (I'm still in the early stages of my Coq journey, so please don't judge my code style too harshly :-P—with that said, any feedback is welcome.)
Last updated: Jun 10 2023 at 06:31 UTC