CS PhD → @UTCompSci, PL/Systems. Jokes → @dijkstracula. Sometimes → @nathan@types.pl . he/him.
Austin, TX
Joined December 2021
- Tweets74
- Following97
- Followers121
- Likes256
curry-howard corresponders: in the evening I've been working through The Little Typer and have been enjoying myself, but using `replace` has me totally flummoxed. Is there a more common name for this dependent function? (It _kind of_ looks like Agda's `subst`, but just barely..?)
2
2
I appreciate usenix's offer to charge grad students multiple hundreds of dollars to not have to go anywhere near Carlsbad
1
1
Maybe there've been students whose virtual conference experience extended beyond "log into the conference's Slack; introduce oneself and log out to never return; watch the public recordings on Youtube, a month later" but I haven't met 'em yet
1
2
New blog post: "Proving The Coding Interview II: toString() 2 furious"
cs.utexas.edu/~ntaylor/blog/…
...aaand here's the third and final Dafny post, where we port Java's `Integer.toString()` method, and prove that it adheres to the specification we wrote in part 2:
cs.utexas.edu/~ntaylor/blog/…
(Does this seem like a lot of work? Well we talk about that in parts 2 and 3 too)
Nathan Taylor retweeted
...aaand here's the third and final Dafny post, where we port Java's `Integer.toString()` method, and prove that it adheres to the specification we wrote in part 2:
cs.utexas.edu/~ntaylor/blog/…
(Does this seem like a lot of work? Well we talk about that in parts 2 and 3 too)
(this was originally a pretty lengthy post that I split into two, so the final part is coming shortly!)
at the start of every meeting with my advisor I put three dollar bills on his desk, taking one away every time he tells me that "once again, we are not going to solve this problem with session types" xitter.cf/ProfRobAnderson/status…
Professors: How do you usually handle tipping in your classes? I write my venmo up on the board the first day so students can express their appreciation for an especially well-delivered lecture. Other ideas worked better for you?
9
Because clearly I haven't been given enough work to do, this past weekend I blogged about formally-verifying a Fizzbuzz cs.utexas.edu/~ntaylor/blog/…
the old "append '...in bed' to a fortune" game, but instead prepend "under Curry-Howard ..." to a seminar discussion question
2
Can't claim to have gotten any research done today, but I did write yet another Vim syntax plugin for yet another research language, so it's impossible to say if I was unproductive or not,
2
11
