Show newer

Various diagonal arguments, such as those found in the proofs of the halting theorem, Cantor's theorem, and Gödel‘s incompleteness theorem, are all instances of the Lawvere fixed point theorem

yoooooo

I think they're like the kind of things like Hedberg's where it's, like, interesting facts about computability/decidability and so on
I'd probably enjoy mechanizing them, if I understood them

Show thread

Martin Escardo tweets a lot of interesting proof threads I don't understand. Might read one of those one day

re: shop talk 

no more paper. I'll probably get to setting up autograding... maybe...

Show thread

re: shop talk 

Why is this paper so long. Why are there 50 pages to review. Who could have possibly done this

(it was me)

Show thread

re: shop talk 

I had previously solved this issue by not explaining the intuition of the syntax until typing rules are presented, which I'm not fond of, because seeing the syntax without explanation will make me ask why? why? why?

Show thread

re: shop talk 

I want to explain what a particular part of the syntax means but I need to appeal to subtyping for the intuition but I need to introduce the syntax to explain subtyping. It is always mutually dependent like this

Show thread

re: shop talk 

I'm tempted to say that "cofixpoints corecursively coconsume a coinductive" lmao

Show thread

re: shop talk 

All of a sudden I'm not too sure what position annotations are for
It seems to me like a leakage of the implementation over to the typing rules, where they aren't actually "used" for anything

Show thread

re: shop talk 

I completely forgot I had marking to do lmao

Show thread

re: shop talk 

Oh I know, I'll highlight important syntax in grey. Genius

Show thread

re: shop talk 

I wrote down that we "define ∞+1 to be equal to ∞" without saying equal in what sense and it feels so wrong

Show thread

shop talk 

I'm gonna edit one of my paper sections and I'm going to livetoot it to entertain myself
This is a preëmptive thread

Me: sends email about the work I'm to do
Me:
Me:
Me: oh that means I need to do that work now huh

A smooth operator is an operator that is infinitely differentiable

why the fuck did phones get rid of the sd card slot give it back

These applications are such a chore (not to mention expensive!) that it's surprising that people will submit applications with minimal idea of what a research program is for or personal statements that incorrectly identify the potential advisor's research topics (usually as ML)
All that time and money spent just to bureaucratically spam a university

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.