Sadly ICFP didn't want this, but maybe you'll find it interesting anyway. https://www.type-driven.org.uk/edwinb/idris-2-quantitative-type-theory-in-action.html … Off I go to the LaTeX mines to make it harder to reject... but not just yet.
-
-
-
-
Replying to @edwinbrady
??? I clicked on "draft", I clicked on the paper title, they both directed to https://www.type-driven.org.uk/papers/idris2.pdf … which 404ed on my end
1 reply 0 retweets 0 likes -
Replying to @ClarissaAdjoint
It seems I don't understand my site generator. I think it's fine now, sorry for the confusion!
1 reply 0 retweets 0 likes -
Replying to @edwinbrady @ClarissaAdjoint
Now there's a missing 'b' after 'edwin'...
1 reply 0 retweets 1 like
Replying to @bentnib @ClarissaAdjoint
I'm definitely giving up for today
8:15 AM - 8 May 2020
0 replies
0 retweets
3 likes
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.