[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
It is also probably worth checking out the work I did on subtyping with Christophe Raffalli. It has been around for a while, but only recently accepted for publication in the TOPLAS journal. The system is an extension of (Curry-style) System F with: - subtyping (obviously), - existential types, - sums and products, - inductive and coinductive types (with ordinal sized), - general recursion with termination checking. On the technical side, our approach mixes: - a new notion of “local subtyping” (with judgments “t : A ⊆ B”), - choice operators similar to Hilbert Epsilon for a simple semantics, - cyclic proofs (shown well-founded with the size-change principle). Here are a couple of links: - https://lepigre.fr/files/publications/LepRaf2018a.pdf (paper), - https://rlepigre.github.io/subml/ (online interpreter), - https://github.com/rlepigre/subml (source code). Cheers, Rodolphe. -- Rodolphe Lepigre <[email protected]> Inria (Deducteam), LSV, CNRS, Université Paris-Saclay, FRANCE https://lepigre.fr On 05/12/18 03:43, Aaron Gray wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I am looking for papers on type inference for mutually recursive algebraic > types with subtyping. > > Many thanks in advance, > > Aaron > -- > Aaron Gray > > Independent Open Source Software Engineer, Computer Language Researcher, > Information Theorist, and amateur computer scientist.
