A type system for embedded rewriting languages with associative pattern matching: from theory to practice

Cláudia Tavares 1, *
* Auteur correspondant
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Programmers are often interested in a way to write error-free programs, i.e. to avoid undesired behaviors. In this context, a type system was conceived as the formal method for speci cation and proof of programs written in the Tom rewriting language. The Tom programming language is an extension of Java that adds pattern matching, more particularly associative pattern matching, and reduction strategies. Accordingly, we aim to make the static typing of the Tom constructs, in particular matching constructs, compatible with the features of Java. This paper presents a type system with nominal subtyping for Tom, that is compatible with the Java type system, and that performs both type inference. We adopted the idea that type inference is a form of type checking and included equality and subtyping constraints inside typing judgments. We propose a constraint-based type inference system to infer types of variables occurring in algebraic terms. Then, we de fine rules to solve equality constraints by uni cation. For the resolution of subtyping constraints, we introduce rules for a combination of constraint propagation, generation of solution and garbage collecting of remaining constraints.
Type de document :
Rapport
[Research Report] 2011, pp.20
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00643808
Contributeur : Cláudia Tavares <>
Soumis le : samedi 3 décembre 2011 - 20:24:04
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : jeudi 30 mars 2017 - 19:56:19

Fichier

Implementation.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00643808, version 2

Collections

Citation

Cláudia Tavares. A type system for embedded rewriting languages with associative pattern matching: from theory to practice. [Research Report] 2011, pp.20. 〈hal-00643808v2〉

Partager

Métriques

Consultations de la notice

196

Téléchargements de fichiers

116