Articulating the ineffable. Programming language theory 
cognitive psychology. PhD @Stanford
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
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 …
Also interested in: - What logics form the core of modern proof assistants? - How is verification done efficiently? e.g. how is SMT integrated? - What are the hard parts of building a real-world proof assistant? e.g. it's easy to make an STLC interpreter, but hard to make OCaml
Not sure if it's what you're looking for, but here's a pretty good tutorial for implementing a dependently typed language https://www.andres-loeh.de/LambdaPi/
Yes, I'd also like to know how much implementing a dependently-typed language would answer my questions. (I have a copy of The Little Typer that I keep meaning to revisit...) The relationship between dependent types <-> theorem proving is still not 100% clear to me.
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/ …
are you considering linear/adjoint logic?
Nothing's off the table! But I'd like to start with whatever logics are most commonly used for proof assistants.
My favourites: * Basics: https://andres-loeh.de/LambdaPi/ * (Relatively) simple version of higher order unification: http://adam.gundry.co.uk/pub/pattern-unify/ … * Implementing dependent type checking using Racket Macros: https://dl.acm.org/doi/10.1145/33 * Another typechecking tutorial: http://www.davidchristiansen.dk/tutorials/nbe/
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
