Comparing Cubes of Typed and Type Assignment Systems (2009)
Steffen Bakel, Simona Ronchi Rocca\lambda, Pawel Urzyczyny
Abstract We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt's typed *-cube [4]. The first is obtained from the latter through applying a natural...
A completeness result for λµ (2009)
Phillipe Audebaud, Steffen Bakel
We study the expressivity of Parigot’s λµ-calculus, and show that each statement Γ ⊢ LK ∆ that is provable in Gentzen’s LK has a proof in λµ. This result is obtained through defining an...
Steffen Bakel, Sjaak Smetsers, Simon Brock
This paper introduces a notion of partial type assignment on left linear applicative term rewriting systems that is based on the extension defined by Mycroft of Curry’s type assignment system. The...
Polymorphic Intersection Type Assignment for RewriteSystems with Abstraction and fi-rule (2008)
Steffen Bakel, Franco Barbanera, Maribel Fern
Abstract We define two type assignment systems for first-order rewriting extended with application, *-abstraction,and fi-reduction, using a combination of intersection types and second-order...
Steffen Bakel, Luigi Liquori, Simona Ronchi, Rocca Paweł Urzyczyn, Afdeling Informatica, Instytut Informatyki
We study the cube of type assignment systems, as introduced in [10]. This cube is obtained from Barendregt’s typed-cube [1] via a natural type erasing function E, that erases type information from...
Department of Computing, Imperial College, (2008)
Steffen Bakel, Franco Barbanera, Mariangiola Dezani-ciancaglini
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,...). Then we prove, in an (almost)...
Strong Normalization of Typeable Rewrite Systems Afdeling Informatica, Universiteit Nijmegen, (2008)
Steffen Bakel, Maribel Fernández
This paper studies termination properties of rewrite systems that are typeable using intersection types. It introduces a notion of partial type assignment on Curryfied Term Rewrite Systems, that...
Comparing Cubes of Typed and Type Assignment Systems (2008)
Steffen Bakel, Luigi Liquori, Simona Ronchi Rocca, Paweł Urzyczyn, Instytut Informatyki, Uniwersytetu Warszawskiego, ...
We study the cube of type assignment systems, as introduced in [13], and confront it with Barendregt’s typed-cube [4]. The first is obtained from the latter through applying a natural type erasing...
Rewrite Systems with Abstraction and-rule: Types, Approximants and Normalization (2008)
Steffen Bakel, Franco Barbanera, Maribel Fernández
In this paper we define and study intersection type assignment systems for first-order rewriting extended with application,-abstraction, and-reduction (). One of the main results presented is that,...
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and -rule (2007)
Steffen Bakel, Franco Barbanera Maribel
We define two type assignment systems for first-order rewriting extended with application, ¤-abstraction, and ¥-reduction, using a combination of intersection types and second-order polymorphic...
A completeness result for λµ (2006)
Phillipe Audebaud, Steffen Bakel
We study the expressivity of Parigot’s λµ-calculus, and show that each statement Γ ⊢LK ∆ that is provable in Gentzen’s LK has a proof in λµ. This result is obtained through defining an...