← Feed

Posts

• Post #2567976

  Cracking myself up over my morning oatmeal imagining if the proof assistant currently known as Rocq had instead been renamed "Le Chicken".

• Post #2334008

  I think one reason why a lot of the academic literature on parsing and grammars is so disconnected from what language implementations use in practice is that what matters is not having a declarative spec for what an instance of the grammar is, what matters is following an algorithm whose failure conditions are understandable. When you implement recursive descent, at the point of a failure you know more or less what is going on. A full declarative specification of what the parser should do in th...

• Post #2202427

  You can find slides for the TYPES2026 talk I just gave on my website: https://owenlynch.org/archive/2026-types/1.html. These slides include hippogriff (https://tangled.org/owenlynch.tngl.sh/hippogriff/) compiled to WASM, so you can edit the code snippets and run them with ctrl-enter to see what happens.

• Post #2103990

  Just picked up from "Logical Relations as Types" the practice of not saying the words "beta rule" and "eta rule" and instead saying "computation rule" and "uniqueness rule". I feel like I would have been much happier if people had used this terminology when I originally learned type theory, and I'm definitely going to use it next time I teach someone. While I'm on that subject... I like th...

• Post #1851325

  What's the minimal way of getting the yo hiragana in LaTeX without fussing too much with fonts, which will work on the arXiv?

• Post #1851324

  In theory, a theoretical problem does not necessarily imply a practical problem, but in practice it almost always does.

• Post #1851323

  When people complain about using category theory for PL, I think about this quote from Cryptonomicon (delivered by the fictional Alan Turing) "Shut up about Leibniz for a moment, Rudy, because look here: You--Rudy--and I are on a train, as it were, sitting in the dining car, having a nice conversation, and that train is being pulled along at a terrific clip by certain locomotives named The Bertrand Russell and Riemann and Euler and others. And our friend Lawrence is running alongside t...

• Post #1851322

  @eigil yo welcome back to civilization

• Post #1851321

  I'm stopping by Utrecht Science Park for the next couple hours; if there are any type theorists who want to chat DM me!

• Post #1805743

  My video on teaching @thosgood how to elaborate the simply typed lambda calculus is up! https://www.youtube.com/watch?v=uBjuFDs-shw&list=PLhgq-BqyZ7i5C6ZnaYiGDhiGZuvvtLh5o&index=9

• Post #1490092

  Whenever I do something fancy with normalization by evaluation I have an urge to shout "Yes closures! Dance for me! Dance! Dance!"

• Post #1490091

  Modal type theory people: Given a judgmental proposition P (that is, not necessarily a type, a meta-level proposition), there is an open modality associated to it which looks like (P -> A), this is right adjoint to adding a proof of P to the context. So far, so good. I want to now instead have a context formation operator which acts like (P -> Γ). My intuition here is that (P -> Γ) "locks" the context Γ, and Γ,P "unlocks" the context. Th...

• Post #1490090

  The observation that I can get trapped by almost any site with an algorithmic feed (YouTube, Twitter, Reddit, hell even Facebook), no matter how asinine the content it gives me, is very humbling to any pretensions of taste that I have... To escape these, the solution has never been to block the relevant domain in ublock, because I inevitably end up wanting to look at some link that someone has sent, and then I unblock it, and then it's off to the races. The solution is also not self con...

• Post #1490089

  Is there a left adjoint to Nakano's later modality? It would be nice to handle it MTT style as a positive modality, rather than just have it as an applicative functor. Perhaps it needs linearity in order to work though, because it's not a monad... @danielgratzer @bentnib