@[email protected]

Open invitation: If you are learning Agda or Martin-Löf type theory and wish to talk about it or related matters, contact me and I will try to help to the best of my ability.

@andrasKovacs6 Congratulations!

I defended my thesis last Friday: andraskovacs.github.io/pdfs/phdthesis…

@TheHalPrince I will. Thank you.

@mietek Check out The Annotated Gödel.

I wish for an annotated guide to Gödel’s incompleteness theorems, written in modern logical notation, by someone familiar with type theory.

The thread to end all threads.

Every time I read some weekend column about a boomer struggling to retire on $100,000 a year and a multi-million dollar home, I'm reminded that my retirement plan is to die in the climate wars.

Find me on libera.chat IRC, in the ##dependent types channel. Mastodon of last resort: @mietek@types.pl

MacPaint Street Scene by G. Clement (1985) #macintosh #apple

"Why are young people all turning left-wing?" Dunno, maybe because older generations expect them to work all hours for bad pay, hand half of it to a landlord for poor quality housing, then stare at a blank wall until they fall asleep - with no real hope of anything better.

Translating proofs from an impredicative type system to a predicative one. ~ Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal. arxiv.org/abs/2211.05700 #ITP

Staged programming with typeclasses. ~ Thomas Bagrel. tweag.io/blog/2022-11-1… #Haskell #FunctionalProgramming

@arntzenius Congratulations!

Termination we ensure just by avoiding unrestricted recursion - nontermination is an effect! Monotonicity we ensure by requiring ALL functions to be monotone, putting Datafun's semantics in Poset, where non-monotonicity is a comonad/coeffect!

My thesis is complete (link downthread)! Also, I have a PhD now. I was going to make a blog post about this but I kept putting it off.

Thesis: rntz.net/files/thesis.p…

The Virtue of Owning Books You Haven't Read: Why Umberto Eco Kept an "Antilibrary" openculture.com/2022/11/the-vi…

Whenever I visit London I’m fascinated by the distinctive sound of the Jubilee Line trains accelerating. Last time I visited, I thought of the idea to turn it into a pad, and it has now become a staple sound in one of my current game projects.

Did Twitter Blue tweet just cost Eli Lilly $LLY billions? Yes.

TIL you can render diagrams on GitHub using markdown 😱 Markdown / Preview

Continuation-passing style, defunctionalization, and hidden appeal of the algebraic property of associativity in Jeremy Gibbons's @jer_gib talk youtu.be/8gnhaE2nmQ0

"with a notable exception of MacOS, MagicCap and Newton OS, operating systems have been thrusting upon a user a flood of disparate interfaces, commands, and actions, all aimed at essentially the same thing: filling in and editing a list or table." okmij.org/ftp/papers/Dre…