Radio and PodcastRadio and PodcastLive Radio & Podcasts
Double-negation translations and CPS conversion, part 2 artwork
Technology

Double-negation translations and CPS conversion, part 2

Iowa Type Theory Commute by Aaron Stump

Apr 2, 202613:31Technology

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...

About This Episode

Double-negation translations and CPS conversion, part 2 is an episode from Iowa Type Theory Commute by Aaron Stump. In this episode, I talk about the control operator callcc, and how it is implemented during compilation using continuation-p...

Podcast

This episode belongs to Iowa Type Theory Commute.

Listen Online

Use the player on this page to stream the episode online.

Episode Details

Published Apr 2, 2026, 13:31 long, audio available.

Related Episodes

Continue listening to more episodes from Iowa Type Theory Commute.

Coercive subtyping and coherence

Jul 1, 2026 - 20:30

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering pers...

A Strange Deal

Apr 30, 2026 - 2:57

The Curry-Howard isomorphism for the law of excluded middle, as a radio drama. I first saw a version of t...

Great paper: The Calculated Typer

Apr 20, 2026 - 23:41

I discuss a nice paper I quite enjoyed reading, called The Calculated Typer , by Garby, Bahr, and Hutton....