Iowa Type Theory Commute

What are commuting conversions in proof theory?


Listen Later

Commuting conversions are transformations on proofs in natural deduction, that move certain stuck inferences out of the way, so that the normal detour reductions (which correspond to beta-reduction under Curry-Howard) are enabled.  The stuck inferences are uses of disjunction elimination.  In programming terms, if you have an if-then-else (a simple case of or-elimination) where the then- and else-branches are lambda abstractions, and you apply that if-then-else to an argument, you need commuting conversions to move the argument into the branches, so you can call the functions (in the then- and else-branches) with it.

See Section 10.1 of Girard's Proofs and Types for more on the problem, and a nice paper by de Groote on strong normalization with commuting conversions.

...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,162 Listeners

Interesting Times with Ross Douthat by New York Times Opinion

Interesting Times with Ross Douthat

7,255 Listeners

Tech Won't Save Us by Paris Marx

Tech Won't Save Us

577 Listeners

Dwarkesh Podcast by Dwarkesh Patel

Dwarkesh Podcast

561 Listeners

The Ezra Klein Show by New York Times Opinion

The Ezra Klein Show

16,536 Listeners

The Haskell Interlude by Haskell Podcast

The Haskell Interlude

14 Listeners

Software Unscripted by Richard Feldman

Software Unscripted

29 Listeners

Oxide and Friends by Oxide Computer Company

Oxide and Friends

69 Listeners