Skip to Main content Skip to Navigation
Reports

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

Cláudia Tavares 1, * 
* Corresponding author
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.
Document type :
Reports
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/hal-00643808
Contributor : Cláudia Tavares Connect in order to contact the contributor
Submitted on : Saturday, December 3, 2011 - 8:24:04 PM
Last modification on : Saturday, June 25, 2022 - 7:43:24 PM
Long-term archiving on: : Thursday, March 30, 2017 - 7:56:19 PM

File

Implementation.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

97

Files downloads

53