On: Type Theory and Functional Programming (1999) [pdf]

[avodonosov]

Have you found this stuff useful during the many years since you learned it? Or you don't mean you mastered it enough to judge its usefulness?

[cjfd → avodonosov]

I have a personal coq/rocq project regarding the verification of software so for that purpose it is highly useful. I also wrote a proof assistent myself (https://github.com/chrisd1977/system).