Dana Scott on Lattice Fixpoint Semantics and Gopal Gupta on Logic, Co-induction and Infinite Computation

Dana Scott gave this talk in 2023, celebrating seventy years of saying absolutely everything.  cf  HRH King Charles III Celebrating Fifty Years of Saying The Same Damned Thing Over and Over Again (that's called "iterating on the bottom", according to Larry Paulson.)

 

Subscribe to Topos Institute.

Gopal Gupta gave this talk on July 25, 2018. See Emily Riehl and Terrence Tau on The Future of Mathematics. Mike Gordon was thinking about these things in February 2017. See Daniel Tubbenhauer on Computational Science.

43:38 Discussion with Yuri Gurevich about the Category theory of this mechanism. Reminds me of something Robin Milner once told me: "You have to know some Category theory because whenever you make something they always want to know what Category it is." In this case the Category theorists were so happy to have something concrete they could actually get their hands on that they did all the Category theory for him! 

51:53 An interpreter for Linear Temporal Logic in one slide. See Moshe Vardi talking about LTLf.

They have a real-time extension which allows verification of real-time systems. In the model, time is a continuous parameter.

Applications include non-monotonic reasoning:

1:08:18 Another discussion with Yuri Gurevich about non-monotonic reasoning. 

See also https://www.microsoft.com/en-us/research/video/logic-co-induction-and-infinite-computation/ and https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction developed after a visit to Gopal's lab in UT Dallas.

I was in Dallas in March, 2023, but not allowed to visit anyone, because my ESTA waiver had been revoked for the crime of not having a credit card. 

Subscribe to Microsoft Research. 

Formalising Graph Algorithms with Coinduction by Donnacha Oisín Kidney and Nicolas Wu. In Volume 9, Issue POPL, January 2025. 

Subscribe to ACM SIGPLAN. 

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

Hitachi HD44780U LCD Display Fonts

Image
I finally got the bit-mapped fonts from the Hitachi "1602" display :  Here's some JavaScript: const HD44780U01ASCII=[ [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ], [4, 4, 4, 4, 0, 0, 4, 0, 0, 0, ], [10, 10, 10, 0, 0, 0, 0, 0, 0, 0, ], [10, 10, 31, 10, 31, 10, 10, 0, 0, 0, ], [4, 15, 20, 14, 5, 30, 4, 0, 0, 0, ], [24, 25, 2, 4, 8, 19, 3, 0, 0, 0, ], [12, 18, 20, 8, 21, 18, 13, 0, 0, 0, ], [12, 4, 8, 0, 0, 0, 0, 0, 0, 0, ], [2, 4, 8, 8, 8, 4, 2, 0, 0, 0, ], [8, 4, 2, 2, 2, 4, 8, 0, 0, 0, ], [0, 4, 21, 14, 21, 4, 0, 0, 0, 0, ], [0, 4, 4, 31, 4, 4, 0, 0, 0, 0, ], [0, 0, 0, 0, 12, 4, 8, 0, 0, 0, ], [0, 0, 0, 31, 0, 0, 0, 0, 0, 0, ], [0, 0, 0, 0, 0, 12, 12, 0, 0, 0, ], [0, 1, 2, 4, 8, 16, 0, 0, 0, 0, ], [14, 17, 19, 21, 25, 17, 14, 0, 0, 0, ], [4, 12, 4, 4, 4, 4, 14, 0, 0, 0, ], [14, 17, 1, 2, 4, 8, 31, 0, 0, 0, ], [31, 2, 4, 2, 1, 17, 14, 0, 0, 0, ], [2, 6, 10, 18, 31, 2, 2, 0, 0,...
Read more

Using Pipewire to Make A Music Synthesizer

Image
Illustration from Project Gutenberg's The Tenniel Illustrations for Carroll's Alice in Wonderland by Sir John Tenniel. Thinking about the linux desktop audio problem: I'm not the only one who finds this weird: https://t.co/b2BZMiak07 — eternal Doorman (@IanANGrant66) May 17, 2025  I noticed that if you change the volume using the Gnome volume keys it changes it in jumps. Usually you don't notice, but if you play a pure sine tone then you can easily hear the distortion. If you want to play with pipewire from C on Ubuntu 24.04 then it's really easy. The pipewire tutorials and examples can be compiled and run if you just first install the pipewire-0.3-dev package with sudo apt install libpipewire-0.3-dev But the API is sooo far away from pluggable, typed streams that I find it quite depressing. Is it because nobody understands the necessary type system . See  Programming Channel Processes and Alice's Adventures In The Wonderland Wide Web . [Update: y...
Read more