MSP Strathclyde Lecure - Conor McBride on Bi-directional Typing

I've only seen 15 minutes of this but it looks like it's going to be a really great lecture. Who invented this stuff? (Thierry Coquand, Benjamin Pierce and David Turner, I think). Google suggests it was a bunch of people hacking on compilers in the 90s. It's funny how you can produce really pretty theories doing stuff like that, isn't it? It's as if there's a kind of implicit discipline of mechanism. There is a survey article here: Bidirectional Typing by Jana Dunfield and Neel Krishnaswami. But note the remark at 1:02:35. Maybe see 4.1. "Turning CCω Bidirectional" of Meven Lennon-Bertrand's PhD Thesis (2022): Bidirectional Typing for the Calculus of Inductive Constructions.

This talk is a lot better than the Metaprogramming in Agda course he gave at Cambridge in 2013. See About Logic - Dependent Types.


 Subscribe to MSP – Strathclyde.

Comments

Post a Comment

Popular posts from this blog

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more

Global Virtual Four Season School in The Foundations of Mathematics and Physics

Image
This is happening everywhere, all year around, just because of the nature of actual Human Knowledge. Invited speakers: a bunch of people who all know what they're talking about . On light and the nature of photographic process: Silver halide crystals only go off when exposed to light at certain frequencies, so the crystals have to be embedded in a glycerine matrix with layers of dye to make the film respond to visible light. Subscribe to  Smarter Every Day 2 . See  Joel Hamkins interviewed on About Logic .
Read more