In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, (co-)inductive (sized) types, and it supports general recursion with termination checking. Despite its Curry-style nature, the system can be (and has been) implemented thanks to new techniques based on choice operators, local subtyping and circular proofs. During the talk, I will give you a flavour of these three ideas. In particular, I will show how choice operators can be used to get rid of free variables (and thus typing contexts), while yielding a clear semantics. I will show how local subtyping can be used to make the system syntax-directed. And I will show how circular proofs may be used to handle (co-)inductive types and (terminating) recursion.

References and links: - paper: http://lepigre.fr/files/docs/lepigre2017_subml.pdf - implementation of the system: https://github.com/rlepigre/subml - online interpreter and examples: https://rlepigre.github.io/subml