The Eternal Doorman

This is absolutely brilliant, and there are lot's of great puns about burgery! My comment:   12:42 No you can't keep your secret things there because that belongs to the CIA. Subscribe to Luke O'Sullivan .

Not many people know who Emil Post was, but his model of computational processes as generating systems is one of the simplest to understand. It sits somewhere between the combinator calculus of Curry and Schönfinkel and Church's Lambda Calculus . See Geoffrey K. Pullum's  Creation myths of generative grammar and the mathematics of [Chomsky's] Syntactic Structures . Post proved his Normal Form Theorem for Post canonical systems which shows that "Given any Post canonical system on an alphabet A , a Post canonical system in normal form can be constructed from it, possibly enlarging the alphabet, such that the set of words involving only letters of A that are generated by the normal-form system is exactly the set of words generated by the original system" . What this shows is that a Post canonical system which generates a language can be abbreviated by adding non-terminal symbols which allow sub-structures to be reused at multiple places, thus potentially ...

I'm quite impressed by Frank Pfenning's Adjoint Functional Language he described at OPLSS'24 . It's a language based on Linear Logic with a co-monadic structure which is a kind of modality with associated adjoints which allow a shift from structural to substructural logics in the types. See  https://www.cs.cmu.edu/~fp/projects.html#adjoint  for details. Subscribe to OPLSS'24 . Both he and Bob Harper are funded by Jane Street . See  Bob Harper's Course on Principles of Programming Languages  and  Frank Pfenning's Course on Linear Logic . Most of what programmers do with general purpose programming languages is only done because of what other people do, and those things are almost always done only because of other things other people have done, and so on and so forth. So the benefits of being able to compose programs from the top-down are quite significant. See How Could One Unify CMU and MIT .  We are heck of a long way from being able to manage the te...

She says you can't cheat the physical laws like conservation of energy. Why not? Will God get angry? Subscribe to Charlotte Moser . Physicists cheat laws of physics all the time. It's the way you do physics: you observe an equation then you infer a mechanism that is behind it that somehow causes it to hold. Some people think this is the basis for all of reality: see A New Kind of Science . See his 2020 paper  Quantised Inertia and Galaxy Rotation from Information Theory . Subscribe to Mike McCulloch .

See  Orbifold notation .  Subscribe to  Istrail Laboratory . 

I mean, how to get the best of the two different philosophies of computation. One is based on typed programming languages and the other on engineering with diagrams . This is about practical computing and the cost and feasibility of software development in general. Here is the problem: We have a lot of algorithms which can all be described abstractly using some sort of pseudocode, or perhaps using some particular language (usually Python!). These algorithms are often well-studied and a lot is known about them in terms of their computational complexity in time and space. Substantive practical software systems invariably employ many such algorithms, often implemented in libraries with more or less well-specified APIs. But very few of these libraries are capable of interoperating because they are either packages written in some specific programming language like Java or Haskell, say, or they are written in C and used as object code, or they are written in an interpreted language like Sc...

He gives a first-hand account of how Per Martin-Löf's 1976  Constructive Mathematics and Computer Programming  was received. Partly answers Emily Riehl's question about the schism between type theory and set theory. See  About Logic Interview with Emily Riehl .  30:43 Why Girard called it System F. See  System Fω and Total Functional Programming  and  System Fω And ML Module Semantics . See also  Lambda Calculus to System-F . 1:17:59  By way of motivating a study of Plotkin's PCF : for all practical purposes, most total functions are no more informative than partial functions. See Blum's Speedup Theorem . Moral "Most total functions are not interesting!"  57:58 One way to look at call by name and call by value as types. The earlier comment he refers to for the context (which is partial computable functions) is at 40:00 . See also  Paul Levy - What Is a Monoid?  and Mike Stay's remarks in  Frank Pfenning's Course on Linea...

I found the guy who was explaining co-clocking to me in that dream I had a week ago: If you get to 54:32 you will see what I mean. He goes to provide an operational semantics for π-calculus in terms of linear logic.  See  Some Talks About Type Theory and Languages . It's a really good course. Here is a playlist of the lectures . The notes and other course materials are still available . Subscribe to Andreas Lynge . In 2017 Frank Pfenning gave some lectures on Substructural Type Systems and Concurrent Programming and in 2019 some  lectures on Session-typed Concurrent Programming . In 2024 he changed tack and did a course  on something he calls Adjoint Functional Programming .  For more of the CMU programming language experience see Bob Harper's OPLSS 22 lectures  . Then just after finding this the Topos Institute seminar was this:   I guess Girard would say that they should beware of logical atrocities. See Pfenning's  Lecture Notes on Fun...

See  About Logic Interview with Emily Riehl  and  Marie Durrieu - Bourbaki n’est pas un homme, ... My comments : 11:55 I think there is evidence in Euclid's Elements that there was an analytic process which preceded the synthetic theory he presented. Aristotle makes this explicit where he talks about the process of division as making the demonstrations obvious. He mentions in particular the proof of proposition 32 "In any triangle, if one of the sides is produced, then the exterior angle equals the sum of the two interior and opposite angles, and the sum of the three interior angles of the triangle equals two right angles." This came from considering lines falling across two parallel lines and is very closely connected with the formulation of the parallel postulate. There are other places where you can clearly see that several propositions are all derived from one drawing which then reappears as you connect the separate propositions together. I don't have my notes w...