Author name cluster

Steffen van Bakel

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

TCS Journal 2008 Journal Article

The heart of intersection type assignment: Normalisation proofs revisited

Steffen van Bakel

This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types for a system with ‘ w and a ≤ -relation that is contra-variant over arrow types. The technique applied is to define reduction on derivations and to show a strong normalisation result for this reduction. From this result, the characterisation of strong normalisation and the approximation result will follow easily; the latter, in its turn, will lead to the characterisation of (head) normalisability.

Details DOI

I&C Journal 2004 Journal Article

Intersection types for explicit substitutions

Stéphane Lengrand
Pierre Lescanne
Dan Dougherty
Mariangiola Dezani-Ciancaglini
Steffen van Bakel

We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of available variable in a term, which is a generalization of the classical notion of free variable.

Details DOI

TCS Journal 2003 Journal Article

Normalization, approximation, and semantics for combinator systems

Steffen van Bakel
Maribel Fernández

This paper studies normalization of typeable terms and the relation between approximation semantics and filter models for Combinator Systems. It presents notions of approximants for terms, intersection type assignment, and reduction on type derivations; the last will be proved to be strongly normalizable. With this result, it is proved that every typeable term has an approximant with the same type, and a characterization of the normalization behaviour of terms using their assignable types is given. Then the two semantics are defined and compared, and it is shown that the approximants semantics is fully abstract but the filter semantics is not.

Details DOI

TCS Journal 2002 Journal Article

Intersection types for λ-trees

Steffen van Bakel
Franco Barbanera
Mariangiola Dezani-Ciancaglini
Fer-Jan de Vries

We introduce a type assignment system which is parametric with respect to five families of trees obtained by evaluating λ-terms (Böhm trees, Lévy-Longo trees, etc.). Then we prove, in an (almost) uniform way, that each type assignment system fully describes the observational equivalences induced by the corresponding tree representation of λ-terms. More precisely, for each family of trees, two λ-terms have the same tree if and only if they get assigned the same types in the corresponding type assignment system.

Details DOI

I&C Journal 1997 Journal Article

Normalization Results for Typeable Rewrite Systems

Steffen van Bakel
Maribel Fernández

In this paper we introduce Curryfied term rewriting systems, and a notion of partial type assignment on terms and rewrite rules that uses intersection types with sorts andω. Three operations on types—substitution, expansion, and lifting—are used to define type assignment and are proved to be sound. With this result the system is proved closed for reduction. Using a more liberal approach to recursion, we define a general scheme for recursive definitions and prove that, for all systems that satisfy this scheme, every term typeable without using the type-constantωis strongly normalizable. We also show that, under certain restrictions, all typeable terms have a (weak) head-normal form, and that terms whose type does not containωare normalizable.

Details DOI

TCS Journal 1995 Journal Article

Intersection type assignment systems

Steffen van Bakel

This paper gives an overview of intersection type assignment for the Lambda Calculus, as well as compares in detail variants that have been defined in the past. It presents the essential intersection type assignment system, that will prove to be as powerful as the well-known BCD-system. It is essential in the following sense: it is an almost syntax directed system that satisfies all major properties of the BCD-system, and the types used are the representatives of equivalence classes of types in the BCD-system. The set of typeable terms can be characterized in the same way, the system is complete with respect to the simple type semantics, and it has the principal type property.

Details DOI

TCS Journal 1992 Journal Article

Complete restrictions of the intersection type discipline

Steffen van Bakel

In this paper the intersection type discipline as defined in Barendregt (1983) is studied. We will present two different and independent complete restrictions of the intersection type discipline. The first restricted system, the strict type assignment system, is presented in Section 2. Its major feature is the absence of the derivation rule (⩽) and it is based on a set of strict types. We will show that these together give rise to a strict filter lambda model that is essentially different from the one presented in Barendregt. We will show that the strict type assignment system is the nucleus of the full system, i. e. for every derivation in the intersection type discipline there is a derivation in which (⩽) is used only at the very end. Finally we will prove that strict type assignment is complete for inference semantics. The second restricted system is presented in Section 3. Its major feature is the absence of the type ω. We will show that this system gives rise to a filter λ I-model and that type assignment without ω is complete for the λ I-calculus. Finally we will prove that a lambda term is typeable in this system if and only if it is strongly normalizable.

Details DOI