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

Artwork

Science Tech Pedro Abreu Type Theory Academia Programming Language

Contenuto fornito da Pedro Abreu. Tutti i contenuti dei podcast, inclusi episodi, grafica e descrizioni dei podcast, vengono caricati e forniti direttamente da Pedro Abreu o dal partner della piattaforma podcast. Se ritieni che qualcuno stia utilizzando la tua opera protetta da copyright senza la tua autorizzazione, puoi seguire la procedura descritta qui https://it.player.fm/legal.

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

20d ago 1:49:42

Condividi

MP3•Pagina principale dell'episodio

Contenuto fornito da Pedro Abreu. Tutti i contenuti dei podcast, inclusi episodi, grafica e descrizioni dei podcast, vengono caricati e forniti direttamente da Pedro Abreu o dal partner della piattaforma podcast. Se ritieni che qualcuno stia utilizzando la tua opera protetta da copyright senza la tua autorizzazione, puoi seguire la procedura descritta qui https://it.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 episodi

#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

Condividi

MP3•Pagina principale dell'episodio

Contenuto fornito da Pedro Abreu. Tutti i contenuti dei podcast, inclusi episodi, grafica e descrizioni dei podcast, vengono caricati e forniti direttamente da Pedro Abreu o dal partner della piattaforma podcast. Se ritieni che qualcuno stia utilizzando la tua opera protetta da copyright senza la tua autorizzazione, puoi seguire la procedura descritta qui https://it.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 episodi

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

Tutti gli episodi

×

Benvenuto su Player FM!

Player FM ricerca sul web podcast di alta qualità che tu possa goderti adesso. È la migliore app di podcast e funziona su Android, iPhone e web. Registrati per sincronizzare le iscrizioni su tutti i tuoi dispositivi.

Ascolta più di 500 argomenti