Philip Wadler - Propositions as Types

This is a really great talk, given at Strange Loop in 2015.

He comes back to this slide several times in the questions, and mentions linear logic and category theory. One question is about probability and proofs:

Then he did a talk on applications of this and Gentzen's idea of the subformula property to embeddings of domain specific languages:


Three years later he did a Part 2 of the talk on Propositions s Types:

Apparently there is a blockchain contract language called Plutus, developed by IOHK that is based on Fω. See  System F in Agda, for fun and profit. See John Searle on Realism for more on status representations and top-down causality (21:46). See also this curious observation about System-T with an infinite reduction relation described in Proofs and Types.

See https://plfa.inf.ed.ac.uk/

Subscribe to Strange Loop.

Valeria de Paiva on Gödel's Dialectica Interpretation of PA in Heyting Arithmetic in System-T (see the final line in Wadler's slide above):


Subscribe to Topos Institute.

Sabine Hossenfelder on an idea of Nicolas Gisin concerning Intuitionistic logic and quantum mechanics:


Subscribe to Sabine Hossenfelder.


See The open past in an indeterministic physics by Flavio Del Santo, Nicolas Gisin.

Subscribe to Thing in Itself.

Subscribe to EJ Falconi.


Comments

Post a Comment

Popular posts from this blog

Live Science - Leonardo da Vinci's Ancestry

Image
... and his posterity too? See  On Communication in Linear Time And Hypertext And The Gospel of Sophia . So it looks like El Cielo of the cistine [sic!😂] chapel is not the limit anymore.  I think I just met one of his descendents. A guy called Versailles Toledo who is from Chiapas. That might explain the murals I mention in my recent untitled post , just before the post mentioning this video. I also just took this photo of Rafael Gonzales, born here in Tecate, B.C., who told me about a spring near here called Agua Fría , half way from Tecate to Loma Tova , where, a few decades ago, people used to go to have barbecues and stuff, but now he thinks it may be private land. If someone reading this has a Facebook account, please write a link to this post onto his FB page. To see why I took the photo, look at his T-shirt and the horse-shoes and ponder this: Subscribe to BeatrizER and her video(s?) about mathematical logic, ... Sounds like Edith (II) Rix has been online all the t...
Read more

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