[TYPES] type inference for mutually recursive algebraic types with subtyping

[Aaron Gray]

On Thu, 6 Dec 2018 at 12:51, Rodolphe Lepigre <rodolphe.lepigre at inria.fr>
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.