Elektrine lite

← Feed

Nathan Taylor

nathan@types.pl

<p>concurrency-liker.</p>

Posts

  • Post #3057014

    And it&amp;#39;s done! I did not expect to write *checks `grep | xargs wc -w` 28,000 words about dependently-typed Fizzbuzz, but here we go. Time to find a more interesting thing to work on in the evenings (debating between doing some Alive-style translation validation in Dafny and embedding LTL in Lean...) The whole series: https://ntaylor.ca/posts/proving-the-coding-interview-lean/

  • Post #3057013

    new blog series: get in, losers, we&amp;#39;re doing reactive programming and temporal logic in lean https://ntaylor.ca/posts/lean-ltl/ (draft, feedback welcome!)

  • Post #3057012

    Boy I’d be embarrassed to have graduated from this department if I’d managed to graduate from this department

  • Post #3057011

    New blog post: good gravy we finally made it to LTL - God this one took FOREVER to write and I still haven&amp;#39;t gotten to FRP yet https://ntaylor.ca/posts/lean-ltl-3/

  • Post #3057010

    Seattle folks: anyone else going up to UW for Mike Dodd’s DLS talk this afternoon?

  • Post #3057009

    New blog post: finally got to the point where I can write the words &amp;quot;curry-howard&amp;quot;, please clap https://ntaylor.ca/posts/lean-ltl-4/