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 @GregMichaelson1
One very useful thing, which is that I can quite easily extend one example to really show the power of dependent/linear types. I just wish they'd also suggested what to take out to make room for it! But I'll manage to work that out for the next submission...
2:50 PM - 8 May 2020
0 replies
0 retweets
4 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.