Iowa Type Theory Commute

Double-negation translations and CPS conversion, part 2


Listen Later

In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-passing style (CPS).  I sketch how CPS conversion (transforming a program with callcc into one in CPS that does not need callcc any more) corresponds to double-negation translation from classical to intuitionistic logic.  The paper I am referencing is here.

...more
View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

19 ratings


More shows like Iowa Type Theory Commute

View all
The Changelog: Software Development, Open Source by Changelog Media

The Changelog: Software Development, Open Source

288 Listeners

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas by Sean Carroll

Sean Carroll's Mindscape: Science, Society, Philosophy, Culture, Arts, and Ideas

4,176 Listeners

Interesting Times with Ross Douthat by New York Times Opinion

Interesting Times with Ross Douthat

7,228 Listeners

Tech Won't Save Us by Paris Marx

Tech Won't Save Us

576 Listeners

Dwarkesh Podcast by Dwarkesh Patel

Dwarkesh Podcast

564 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

16,211 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

15 Listeners

Software Unscripted by Richard Feldman

Software Unscripted

29 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

65 Listeners