The Eternal Doorman

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 Functional Comp...

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...

Subscribe to  L'Institut Henri Poincaré . 

I wonder whether this can ever happen with sound or light? Here water is being modeled as a homogeneous fluid. See  All About Water and Entropy .  Subtitle could be "The perfectly reasonable ineffectiveness of mathematics in the physical sciences".  There is a French video platform for mathematics lectures  https://www.carmin.tv/​ Subscribe to  IHES .  After watching that talk I found these and it struck me that composed together they're a kind of inverse to the above problem:  In higher-order ambisonic systems sometimes you get ill-conditioning in the decoder and this produces rogue waves ( 27:37 ). The way these systems work is that they either record from a single point at the center of the space and play back from a shell surrounding the space, or they record from a shell surrounding the space and play back from a central point.  Subscribe to  EMPAC .  Persi Diaconis on Poincaré and probabity.  Poincaré analysed the probability ...

These are all very closely related, but the premisses in each case are different enough that it would take a lot to explain the connection in any detail. I don't know what the answer to this is, except to note that they all have to answer to different funding sources. See  A New Kind of Science . Andrej Bauer - Derivations as Computations See  https://www.andromeda-prover.org/ See also the SEP entry on  Substructural Logic .    Subscribe to ACM SIGPLAN .  Philip Wadler on Interpreters for free 27:13 Whilst trying to explain the idea of proving progress in a reduction relation he gets his slide projector software into a mode where it only allows him to step forwards, ...  See the book  https://github.com/plfa/plfa.github.io Subscribe to INI . An interesting talk on basic Stone duality See also  Stefan Milius - Demystifying Codensity Monads through Duality . Overview of Petri Nets and Derivations Subscribe to MSP Strathclyde .

I can imagine a process where one could use a metalanguage to derive syntactic structures with certain formal properties induced by formal maps between them. This is how I imagine Grothendieck toposes are used in Lawvere's categorical semantics. The way this would work would be like the module system in a high-level functional programming language where one could instantiate syntactic structures at any level by  concrete syntactic objects, which might be derivations in some formal deduction system, or they might be programs-cum-proofs in some type theory, or a construction in some algebraic language like a diagram algebra. However what I imagine is not a single formal system one could download and compile. Rather it would be a network of interconnected systems where syntactic structures defined in one place can be instantiated in many others. So it would not grow monolithically like a proof library, but organically like an ecosystem.    Subscribe to The Well . For more pr...

It's way more interesting than any textbook would have you believe! See  The electric storm of November 1882 . Subscribe to  Dr. Jorge S. Diaz .