Posts

David Knothe and Oliver Bringmann - Combining Big and Small-Step Semantics to Verify Loop Optimizations

Image
See the paper at https://arxiv.org/abs/2602.19868 :   See Patrick Cousot & Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2--3):103--179, 1992 , and also Coinductive big-step operational semantics by Xavier Leroy and Hervé Grall and Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment by David M. Kahn, Jan Hoffmann and Runming Li.   Starts at around 3 hours .  See also  Patrick Bahr - Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations .  Subscribe to ACM SIGPLAN .

Matther Flatt on Rhombus and Racket

Image
He left the ML part of the conference and today he's in the scheme bit, ... See Matthew Flatt on Rhombus and Syntax Transformers .  It's the first talk but YouTube's stupid interface won't let me see the time since the start of the stream until it's over, it only shows relative times from the end of the stream and so all I can tell you is that's around -1:56:43 when the stream start is at about -2:56:04 so maybe around 1:00:00 ? It's interesting to compare this with S. W. P. Steen's definition of a formal system he wrote in 1971. He went to great lengths to define the notion of a symbol, even including explicit metalanguage syntax for concatenation in generated symbols (because he needed to use x, x', x'', x''', ... for fresh variables) then defining type symbols Church-style using a structural induction over concatenated sequences. But for some reason he didn't feel the need to talk about subscripting symbols with type...

Amr Sabry - What is "Quantum" about Quantum Computing?

Image
This is one of the first times I've heard a talk about this that actually seems to make some sense! Starts around 20:00 . 42:54 See Baker's paper NREVERSAL of Fortune - The Thermodynamics of Garbage Collection . Also  Theseus : A High Level Language for Reversible Computing  by Roshan P. James. See Free Quantum Computing by Jacques Carette, Chris Heunen, Robin Kaarsgaard, Neil J. Ross and Amr Sabry,  A computational interpretation of compact closed categories: reversible programming with negative and fractional types  by Chao-Hong Chen and Amr Sabry and Compositional Reversible Computation by Jacques Carette, Chris Heunen, Robin Kaarsgaard and Amr Sabry. 1:08:00 On the reversibility thing, it's weird, isn't it? See the bit starting at at page 18 of  EWD12345 . Nobody ever said anything to me about that. I guess it's a bit weird, but I don't care. I really enjoyed writing it, even though I was quite literally starving at the time. 1:16:42  On measuremen...

Attila Egri-Nagy on a Concatenative Logic Programming Language

Image
Starts at  2:20:06 . See  con-cat An experimental functional concatenative programming language inspired by Joy  and  Joy: Forth’s Functional Cousin by Manfred von Thun .  See also  Two Great Talks on Programming Languages .  Subscribe to ACM SIGPLAN . 

YouTube Click Fraud - Generating Fake Ad Clicks

Image
If you pay YouTube for advertising you should seriously consider a class-action law suit. The way it works is that in the YouTube mobile app they put one of their standard controls "V" under an ad-click link in the top-left corner, so when people don't want your ad and don't want to continue watching the video they get sent to your ad and you pay for the click. The only way for users to get back to the screen they came from is to either wait for the ad to finish, then click the "V" or click the "back" button.  In case they say it's not the meaning of "V" to minimise the player, it is: It's there all through the video, any time you touch the screen. YouTube are just a bunch of crooks.

Karl Voit - Managing Your Personal Information

See  Basics of Personal Information Management: Finding the best tool(s)  and  https://karl-voit.at/ . It's also on GooTube and my comment there was: "I am enlightened and also a bit dismayed to hear how badly I have been doing this whole computer-using thing! 😂"  We could do so much better than the crappy pile of garbage we have right now! See  The T.H.E. Mutiprogramming System Console Message Interpreter  and  Edger W. Dijkstra's 1972 Turing Award Lecture . 

Edger W. Dijkstra's 1972 Turing Award Lecture

Image
Programming languages as vehicles for thought. See  Matthew Flatt on Rhombus and Syntax Transformers  and  The T.H.E. Mutiprogramming System Console Message Interpreter .  Some parts are missing. See the transcript  EWD 340 . 5:42​ "The overwhelming problem was to get and keep the machine in working order. The preoccupation with the physical aspects of automatic computing is still reflected in the names of the older scientific societies in the field, such as the Association for Computing Machinery or the British Computer Society, names in which explicit reference is made to the physical equipment. What about the poor programmer? " 25:46​ "vastly different from what it has been up till now, so different that we had better prepare ourselves for the shock. Let me sketch for you one of the possible futures. At first sight, this vision of programming in perhaps already the near future may strike you as utterly fantastic. Let me therefore also add the considerations t...

Matthew Flatt on Rhombus and Syntax Transformers

Image
Starts around 33 minutes in. Audio is awful for the first few minutes. I'm not sure whether this is really about Rhombus or Racket, ... It's mostly about syntax languages, but here they're even more than syntax languages because they act at the lexical level as well. They even have a notion of lexical scope. I guess it's the original notion of lexical scope! See The Syntax Model in Racket and  Binding as Sets of Scopes . Subscribe to ACM SIGPLAN .

Daan Leijen - Efficient strong functional programming with effects and compiler guided reference counting

Image
This is really interesting. Talk starts at 18:05 or so. See Efficient strong functional programming with effects and compiler guided reference counting  and https://github.com/microsoft/mimalloc . When I tried to look up these projects this morning I got this: Subscribe to ACM SIGPLAN . 

Stephanie Weirich on Functional / Logic Programming in Verse

Image
This is an amazing phenomenon. This language kind of invents type systems as it goes,... It's a bit like what set theorists do, in fact. More on that later,... The talk starts around 34:50 . See  The Verse Calculus: a core calculus for functional logic programming . Also Simon Peyton-Jones' lectures at OPLSS 2026:  Types, Proofs, and Program Logics .  On denotational semantics see also Domain-Theoretic Semantics for Functional Logic Programming : 17:23 On models which are termination-insensitive. See  Two Great Talks on Programming Languages , in particular Shriram Krishnamurthi on the 1991 paper On the expressive power of programming languages by Matthias Felleisen. Subscribe to  ACM SIGPLAN .