Iowa Type Theory Commute

Type inference with simple subtypes

Aaron Stump Season 4 Episode 12

In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell.  The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus.  I mostly focus here on how subtype constraints allow typing any term (which seems surprising).

You can join the telegram group for discussion related to the podcast.