Are there any good resources for building your own proof assistant? I don't really get Coq vs. Lean vs. F* vs. Idris, but I feel like I would get it more from building a pedagogical implementation. e.g. Mini-Pyro was really useful for understanding PPLs: https://pyro.ai/examples/minipyro.html …
-
Show this thread
Replying to @wcrichton
Jeremy Avigad taught a course (I didn't take) in the philosophy dept 2 semesters ago. Unfortunately the online syllabus is sparse but you could reach out to him for the material? http://www.andrew.cmu.edu/user/avigad/itp/ …
12:58 PM - 5 Mar 2020
0 replies
0 retweets
1 like
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.