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

[ 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.