[TYPES] type inference for mutually recursive algebraic types with subtyping
rodolphe.lepigre at inria.fr
Thu Dec 6 07:51:07 EST 2018
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 Lepigre <rodolphe.lepigre at inria.fr>
Inria (Deducteam), LSV, CNRS, Université Paris-Saclay, FRANCE
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 Gray
> Independent Open Source Software Engineer, Computer Language Researcher,
> Information Theorist, and amateur computer scientist.
More information about the Types-list