Emily Riehl Doing Stratospheric Category Theory

Oh God, I think I'm falling in love again, ... See Emily Riehl on Univalent Foundations.


She says there's a joke that goes "In Category Theory you have to give examples of your examples, ..." At 12:29 she gives an example of an extension type:

Check the timestamps!

 

And then she says "And that's the rest of the proof but nobody cares about that."

See Yoneda for ∞-categories and https://rzk-lang.github.io/rzk.

Here is her lecture on fomalising 'post-rigorous mathematics':

 
Here's a proof in infinity-categories:
 ... and another, of the same theorem
 ... and another

Here's Joseph Urban talking about auto-formalisation:


McCarthy, 1962! Poor guy, he was just doing some sort of weird dance in front of an alien from another dimension!

Subscribe to Hausdorff Center for Mathematics

Drinking whisky with Eugenia Cheng last night:


The problem as I recall is with the LALR(n) parser generator that Moscow ML uses. It resolves reduce-reduce conflicts in a random order, so the actual parse tree returned by the generated parser can be different for three different specifications of exactly the same grammar and which one you get depends on the symbolic names of the non-terminals used or the order in which they appear in the definition of the syntax.  See The Moscow ML Owner's Manual. I checked and Claudio Russo's supervisor was Don Sanella at Edinburgh but he worked for Andy Pitts at Cambridge for a while. See Earley Parser which uses dynamic programming (not linear programming!)  See Earley's 1968 PhD thesis An Efficient Context-free Parsing Algorithm and Larry Paulson's 1981 PhD thesis (untitled). It's important that the abstract syntax your compiler extracts from the program source is actually correct. See Tim Griffin's slides for the Cambridge undergraduate course Compiler Construction:



Comments

Popular posts from this blog

Live Science - Leonardo da Vinci's Ancestry

David Turner Obituary by Sarah Nicholas Fri 24 Nov 2023