Search a title or topic

Over 20 million podcasts, powered by 

Player FM logo
Artwork

Content provided by Aaron Stump. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Aaron Stump or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ppacc.player.fm/legal.
Player FM - Podcast App
Go offline with the Player FM app!

More on observational type theory

13:43
 
Share
 

Manage episode 358719408 series 2823367
Content provided by Aaron Stump. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Aaron Stump or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://staging.podcastplayer.com/legal.

I continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality type), and how proofs of equalities can be used to cast terms from one type to another.
Also, in exciting news, I created a Telegram group that you can join if you want to discuss topics related to the podcast or particularly podcast episodes. I will be monitoring the group. I believe you have to request to join, and then I approve (it might take me until later in the day to do that, just fyi). The invitation link is here.

  continue reading

175 episodes

Artwork
iconShare
 
Manage episode 358719408 series 2823367
Content provided by Aaron Stump. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by Aaron Stump or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://staging.podcastplayer.com/legal.

I continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality type), and how proofs of equalities can be used to cast terms from one type to another.
Also, in exciting news, I created a Telegram group that you can join if you want to discuss topics related to the podcast or particularly podcast episodes. I will be monitoring the group. I believe you have to request to join, and then I approve (it might take me until later in the day to do that, just fyi). The invitation link is here.

  continue reading

175 episodes

All episodes

×
 
Loading …

Welcome to Player FM!

Player FM is scanning the web for high-quality podcasts for you to enjoy right now. It's the best podcast app and works on Android, iPhone, and the web. Signup to sync subscriptions across devices.

 

Listen to this show while you explore
Play