Post #1942212

@mevenlennonbertrand This is a really neat paper! I especially appreciated the explanation of the difference between the two different kinds of normal forms in STLC with sums. (And of course, the connections between bidirectional typing and interpolation is natural when you see it.)