Steffen Van Bakel, Franco Barbanera, Maribel Fern
Abstract. We define two type assignment systems for first-order rewriting ex-tended with application, *-abstraction, and fi-reduction (TRS + fi). The typesused in these systems are a combination of...
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...
A Constructive Valuation Semantics for Classical Logic (2008)
Franco Barbanera, Stefano Berardi
Abstract The paper presents a constructive interpretation for proofs in classical logic of \Sigma 01 sentences and for a witness extraction procedure based on Prawitz's reduction rules.
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)...
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,...
A Full Continuous Model of Polymorphism (2008)
Franco Barbanera, Stefano Berardi
Abstract. We introduce a model of the second-order lambda calculus. Such a model is a Scott domain whose elements are themselves Scott domains, and in it polymorphic maps are interpreted by generic...
Abstract Space-Aware Ambients and Processes ⋆ (2008)
Franco Barbanera, Michele Bugliesi, Vladimiro Sassone
Resource control has attracted increasing interest in foundational research on distributed systems. This paper focuses on space control and develops an analysis of space usage in the context of an...
Ali S. Aoun, Mariangiola Dezani-ciancaglini, Seref Mirasyedioglu, Franco Barbanera, Franco Barbanera
Parallelism and non-determinism are fundamental concepts in the process algebra theory. Combining them with-calculus can enlighten the theory of higher-order process algebras. In recent papers an...
Steffen Van 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 (Bohm trees, L'evy-Longo trees, ...). Then we prove, in an (almost)...
Rewrite Systems with Abstraction and β-rule: Types, Approximants and Normalization (2007)
Steffen Van 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 fi-reduction (TRS fi). One of the main results presented...
"Classical" programming-with-proofs in $\lambda^{Sym}_{PA}$: an analysis of non-confluence (2007)
Franco Barbanera, Stefano Berardi, Massimo Schivalocchi
. Sym PA is a natural deduction system for Peano Arithmetic that was developed in order to provide a basis for the programmingwith -proofs paradigm in a classical logic setting. In the paper we...
A Constructive Valuation Semantics for Classical Logic (2007)
Franco Barbanera, Stefano Berardi
The paper presents a constructive interpretation for proofs in classical logic of \Sigma 0 1 sentences and for a witness extraction procedure based on Prawitz's reduction rules. 1 Introduction...
The Simply-Typed Theory of β-conversion has no maximum extension (2007)
Franco Barbanera, Stefano Berardi
It is proved that no maximum consistent extension exists for the simply-typed theory of fi-conversion. 1 Introduction In this paper we address the problem of the existence of a maximum consistent...
Type Assignement for Mobile Objects (2007)
Franco Barbanera, Ugo D'Liquoro
We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for object-oriented sequential programming. For the sake of...
Type Assignement for Mobile Objects (2007)
Franco Barbanera, Ugo De'Liguoro
We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for object-oriented sequential programming. For the sake of...
WOOD’03 Preliminary Version Can Addresses be Types? (a case study: objects with delegation) (2007)
Christopher Anderson, Franco Barbanera, Mariangiola Dezani-ciancaglini, Sophia Drossopoulou
We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to...
Intersection Types and Lambda Models (2005)
Fabio Alessi, Franco Barbanera
Invariance of interpretation by #-conversion is one of the minimal requirements for any standard model for the #-calculus. With the intersection type systems being a general framework for the study...
Alias and Union Types for Delegation (2003)
Christopher Anderson, Franco Barbanera
We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) or finite "unions" of...
Can Addresses be Types? (a case study: objects with delegation) (2003)
Christopher Anderson, Franco Barbanera, Mariangiola Dezani-ciancaglini, Sophia Drossopoulou
We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to...
Alias and Union Types for Delegation (2003)
Christopher Anderson, Franco Barbanera, Mariangiola Dezani-ciancaglini
Abstract — We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) or finite...
Intersection Types and Computational Rules (2003)
Fabio Alessi Franco, Franco Barbanera, Mariangiola Dezani-ciancaglini
The invariance of the meaning of a #-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements one expects to hold for a #-model. Being the intersection...
Alias and Union Types for Delegation (2003)
Christopher Anderson, Franco Barbanera
We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) or finite "unions" of...
A Type Inference Algorithm for Secure Ambients (2002)
Franco Barbanera, Mariangiola Dezani-ciancaglini, Ivano Salvo, Vladimiro Sassone
We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We...
A Type Inference Algorithm for Secure Ambients (2001)
Franco Barbanera, Mariangiola Dezani-ciancaglini, Ivano Salvo, Vladimiro Sassone
We present a bottom-up algorithm which, given an untyped process P , calculates the minimal set of constraints on security levels such that all the actions during a run of P can be performed without...
Steffen Van Bakel, Franco Barbanera, Maribel Fernández
Abstract. We define two type assignment systems for first-order rewriting extended with application,-abstraction, and-reduction (TRS). The types used in these systems are a combination of (-free)...
Intersection Types for λ-Trees (2000)
Steffen Van 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 (Bohm trees, L'evy-Longo trees, ...). Then we prove, in an (almost)...
Intersection Types for λ-Trees (2000)
Steffen Van 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 (Bohm trees, Levy-Longo trees, ...). Then we prove, in an (almost)...
Intersection Types for λ-Trees (1999)
Steffen Van 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 (Bohm trees, Levy-Longo trees, ...). Then we prove, in an (almost)...
Steffen Van 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 (Bohm trees, Levy-Longo trees, ...). Then we prove, in an (almost)...
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 (Bohm trees, Levy-Longo trees, ...). Then we prove, in an (almost)...
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 (Bohm trees, Levy-Longo trees, ...). Then we prove, in an (almost)...
A Constructive Valuation Semantics for Classical Logic (1996)
Barbanera, Franco, Berardi, Stefano
This paper presents a constructive interpretation for the proofs in classical logic of $\Sigma^0_1$ -sentences and for a witness extraction procedure based on Prawitz's reduction rules.
Modularity of Strong Normalization in the Algebraic-lambda-cube (1996)
Uperieure S Ormale, N Ecole, The Algebraic--cube, Franco Barbanera, Franco Barbanera, Maribel Fernández, ...
In this paper we present the algebraic-lambda-cube, an extension of Barendregt's lambda-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular...
A Strong Normalization Result for Classical Logic (1995)
Franco Barbanera, Stefano Berardi
In this paper we give a strong normalization proof for a set of reduction rules for classical logic. These reductions, more general then the ones usually considered in literature, are inspired to the...
Modularity of Strong Normalization and Confluence in the algebraic-lambda-cube (1994)
Franco Barbanera, Maribel Fernández, Herman Geuvers
In this paper we present the algebraic--cube, an extension of Barendregt's -cube with first- and higherorder algebraic rewriting. We show that strong normalization is a modular property of all...
Steffen Van Bakel, Franco Barbanera, Maribel Fern
ion and fi-rule ? Extended Abstract Steffen van Bakel 1 , Franco Barbanera 2 , and Maribel Fernandez 3 1 Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ....
Steffen Van Bakel, Franco Barbanera, Maribel Fern
ion and fi-rule Extended Abstract Steffen van Bakel 1 , Franco Barbanera 2 , and Maribel Fernandez 3 1 Department of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ, svb@doc.ic.ac.uk 2...
Extracting Constructive Content from Classical Logic via Control-like Reductions
Franco Barbanera, Stefano Berardi
. Recently there has been much interest in the problem of finding the computational content of classical reasoning. One of the most appealing directions for the computer scientist to tackle such a...