Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice

Zena M. Ariola, Paul Downen, Hugo Herbelin

Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural core…