Practical Subtyping for System F

Carte non disponible

Date/heure
Date(s) - 17/11/2016
11 h 00 min - 12 h 00 min

Catégories Pas de Catégories


We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and coinductive types. Inductive and coinductive types may carry size annotations allowing the preservation of size invariants. For example it is possible to derive the termination of the quick sort by showing that partitioning a list does not increase its size. The system is able to deal with complex programs involving mixed induction and coinduction, or even mixed (co-)induction and polymorphism (as for Scott-encoded datatypes). One of the key ideas is the use of symbolic witnesses to handle quantifiers of all sorts. To demonstrate the practicality of our system, we provide an implementation that accepts all the examples discussed in the paper and more.

http://www.lama.univ-savoie.fr/~raffalli/

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange