System Fω And ML Module Semantics

Followup to Compiler Coffee Club - Interning Cyclic Types in a Compiler.

I listened to this talk by Bob Harper and learned about this paper by Rossberg, Russo and Dreyer. See https://people.mpi-sws.org/~rossberg/f-ing/ and for some background: https://sdiehl.github.io/typechecker-zoo/system-f-omega/system-f-omega.html. See also Xavier Leroy's slides for his course Programming = proving? which are very readable: Polymorphism all the way up! From System F to the Calculus of Constructions.

13:42 I spent many, many hours trying to solve this problem in exactly the same context, using the same language! It just never occurred to me to do the type inheritance bottom-up. I should have read his book! See page 185 Functors and Sharing Specifications. 

Subscribe to Topos Institute.