[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Thu, 6 Dec 2018 at 12:51, Rodolphe Lepigre <[email protected]> wrote: > 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). > Rodolphe, This is great exactly what I was looking for plus more covering coinduction in a very clever way. Its great to have an implementation too as well. Many thanks I think I will be use this. Regards, Aaron 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. > -- Aaron Gray Independent Open Source Software Engineer, Computer Language Researcher, Information Theorist, and amateur computer scientist.
