#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen Type Theory Forall podcast

Artwork

Science Tech Pedro Abreu Type Theory Academia Programming Language

Innehåll tillhandahållet av Pedro Abreu. Allt poddinnehåll inklusive avsnitt, grafik och podcastbeskrivningar laddas upp och tillhandahålls direkt av Pedro Abreu eller deras podcastplattformspartner. Om du tror att någon använder ditt upphovsrättsskyddade verk utan din tillåtelse kan du följa processen som beskrivs här https://sv.player.fm/legal.

Type Theory Forall »
#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

20d ago 1:49:42

Dela

MP3•Episod hem

Innehåll tillhandahållet av Pedro Abreu. Allt poddinnehåll inklusive avsnitt, grafik och podcastbeskrivningar laddas upp och tillhandahålls direkt av Pedro Abreu eller deras podcastplattformspartner. Om du tror att någon använder ditt upphovsrättsskyddade verk utan din tillåtelse kan du följa processen som beskrivs här https://sv.player.fm/legal.

In this episode we continue our conversation with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer.

He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris.

In today’s episode we talk about the story behind writing The Little Typer together with Dan Friedman, and we get more technical by talking about Equality, Bidirectional Type Checking, Quotation and Quasi Quotation.

Some links: David's Website David's X Lean Zulip Chat Truth of a proposition, evidence of a judgement, validity of a proof

… continue reading

78 episoder

#Science #Tech #Pedro Abreu #Type Theory #Academia #Programming Language

Artwork

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

Type Theory Forall

27 subscribers

published 20d ago

Dela

MP3•Episod hem

Innehåll tillhandahållet av Pedro Abreu. Allt poddinnehåll inklusive avsnitt, grafik och podcastbeskrivningar laddas upp och tillhandahålls direkt av Pedro Abreu eller deras podcastplattformspartner. Om du tror att någon använder ditt upphovsrättsskyddade verk utan din tillåtelse kan du följa processen som beskrivs här https://sv.player.fm/legal.

In this episode we continue our conversation with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer.

He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris.

In today’s episode we talk about the story behind writing The Little Typer together with Dan Friedman, and we get more technical by talking about Equality, Bidirectional Type Checking, Quotation and Quasi Quotation.

Some links: David's Website David's X Lean Zulip Chat Truth of a proposition, evidence of a judgement, validity of a proof

… continue reading

78 episoder

#Science #Tech #Pedro Abreu #Type Theory #Academia #Programming Language

Alla avsnitt

×

Välkommen till Player FM

Player FM scannar webben för högkvalitativa podcasts för dig att njuta av nu direkt. Den är den bästa podcast-appen och den fungerar med Android, Iphone och webben. Bli medlem för att synka prenumerationer mellan enheter.

Lyssna på 500+ ämnen