← Feed

Posts

• View post

  Man this post took forever to get out the door but I think I have cornered the market on “formal modelling of pre-i386 memory addressing in Lean” blog posts https://ntaylor.ca/posts/lean-ltl-6/

• View post

  Wild that Jane Street’s new formal methods team is calling out refinement types as something they want experience with- anybody know if there’s someone in particular driving that?

• View post

  thank’s

• View post

  And it'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/

• View post

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

• View post

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

• View post

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

• View post

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

• View post

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