Intersection and Union Types in the (2008)
Daniel J. Dougherty, Silvia Ghilezan, École Normale, Supérieure Lyon
λµ�µ-calculus
Daniel Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec
normalization of the dual classical sequent calculus
Reducibility: a ubiquitous method (2008)
Silvia Ghilezan, École Normale, Supérieure Lyon, Silvia Likavec
in lambda calculus with intersection types
Daniel Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec
normalization of the dual classical sequent calculus
A General Technique for Analyzing Termination in Symmetric Proof Calculi (2008)
Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne
Abstract. Proof-term calculi expressing a computational interpretation of classical logic serve as tools for extracting the constructive content of classical proofs and at the same time can be seen...
Extensions of the Reducibility Method (2008)
Silvia Ghilezan, Silvia Likavec
A general method is developed for proving reduction properties of untyped lambda terms. It is an extension of the reducibility method for typed lambda terms which leads to uniform proofs of...
Security Types for Dynamic Web Data ⋆ (2008)
Mariangiola Dezani-ciancaglini, Silvia Ghilezan, Jovanka Pantović
Abstract. We describe a type system for the Xdπ calculus, introduced in [8]. An Xdπ-network is a network of locations, where each location consists of both a data tree (which contains scripts and...
Reducibility: a ubiquitous method (2008)
Silvia Ghilezan, École Normale, Supérieure Lyon, Silvia Likavec
in lambda calculus with intersection types
Lambda Terms for Natural Deduction, Sequent Calculus and Cut Elimination (2007)
Cut Elimination, Henk Barendregt, Silvia Ghilezan, Silvia Ghilezan
It is well-known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover normalising these terms corresponds to eliminating cuts in the equivalent sequent...
Reducibility Method for Simple Types and Church-Rosser Property (2007)
Abstract. A general reducibility method for proving properties of the simply typed lambda calculus is presented and sucient conditions for its application are derived. This method leads to uniform...
Reducibility Method for Intersection Types (2007)
Silvia Ghilezan, Silvia Likavec
A general reducibility method for proving reduction properties of lambda terms typeable with intersection types is presented. Sucient conditions for its application are derived. This method leads to...
Under consideration for publication in J. Functional Programming 1 THEORET I CAL PEARLS (2007)
Cut Elimination, Henk Barendregt, Silvia Ghilezan, Silvia Ghilezan
Lambda terms for natural deduction, sequent
NATURAL DEDUCTION AND SEQUENT TYPED LAMBDA CALCULUS (2007)
Two different formulations of the simply typed lambda calculus: the natural deduction and the sequent system, are considered. An analogue of cut elimination is proved for the sequent lambda calculus.
Security Types for Dynamic Web Data (2007)
Dezani-Ciancaglini, Mariangiola, Ghilezan, Silvia, Pantovic, Jovanka, Varacca, Daniele
We describe a type system for the Xdpi calculus. An Xdpi-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at...
Security Types for Dynamic Web Data (2007)
Dezani-Ciancaglini, Mariangiola, Ghilezan, Silvia, Pantovic, Jovanka, Varacca, Daniele
We describe a type system for the Xdpi calculus. An Xdpi-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at...
Characterizing strong normalization in a language with control operators. (2004)
Dougherty, Dan, Ghilezan, Silvia, Lescanne, Pierre
(eng) We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's lambda-mu-mu~. The original lambda-mu-mu~ has a system of...
Two behavioural lambda models (2003)
Mariangiola Dezani-ciancaglini, Silvia Ghilezan
Abstract. We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms. This is proved by using...
Two Behavioural Lambda Models (2003)
Mariangiola Dezani-ciancaglini, Silvia Ghilezan
We build two inverse limit lambda models which characterize completely sets of terms having similar computational behaviour. More precisely for each one of these sets of terms there is a...
Reducibility: a ubiquitous method in lambda calculus with intersection types (2002)
Silvia Ghilezan, École Normale, Supérieure Lyon, Silvia Likavec
A general reducibility method is developed for proving reduction properties of lambda terms typeable in intersection type systems with and without the universal type #. Su#cient conditions for its...
A Lambda Model Characterizing Computational Behaviours of Terms (2001)
Mariangiola Dezani-ciancaglini, Silvia Ghilezan
We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms.
Lambda Models Characterizing Computational Behaviours of Terms (2001)
Mariangiola Dezani-ciancaglini, Silvia Ghilezan
We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms. This is proved by using the...
Lambda Terms for Natural Deduction, Sequent Calculus and Cut Elimination (1998)
Henk Barendregt, Silvia Ghilezan
It is well-known that there is a good correspondence between natural deduction derivations and typed lambda terms. Moreover normalizing these terms is equivalent to eliminating cuts in the...
The "Relevance" of Intersection and Union Types (1997)
Dezani-Ciancaglini, Mariangiola, Ghilezan, Silvia, Venneri, Betti
The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style...
Strong Normalization and Typability with Intersection Types (1996)
A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems.
Inhabitation in Intersection and Union Type Assignment Systems (1993)
Union does not correspond to intuitionistic disjunction and intersection does not correspond to intuitionistic conjunction. The Curry–Howard isomorphism between types inhabited in the intersection...
Abstract. This paper revisits the results of Barendregt and Ghilezan [3] and generalizes them for classical logic. Instead of λ-calculus, we use here λµ-calculus as the basic term calculus. We...