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

Pedro Abreu द्वारा प्रदान की गई सामग्री. एपिसोड, ग्राफिक्स और पॉडकास्ट विवरण सहित सभी पॉडकास्ट सामग्री Pedro Abreu या उनके पॉडकास्ट प्लेटफ़ॉर्म पार्टनर द्वारा सीधे अपलोड और प्रदान की जाती है। यदि आपको लगता है कि कोई आपकी अनुमति के बिना आपके कॉपीराइट किए गए कार्य का उपयोग कर रहा है, तो आप यहां बताई गई प्रक्रिया का पालन कर सकते हैं https://hi.player.fm/legal।

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

16d ago 1:49:42

साझा करें

MP3•एपिसोड होम

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

78 एपिसोडस

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