Sciweavers

Share
ENTCS
2002
91views more  ENTCS 2002»
8 years 7 months ago
Subtyping in Logical Form
By using intersection types and filter models we formulate a theory of types for a -calculus with record subtyping via a finitary programming logic. Types are interpreted as space...
Ugo de'Liguoro
ENTCS
2002
66views more  ENTCS 2002»
8 years 7 months ago
Strongly Normalising Cut-Elimination with Strict Intersection Types
This paper defines reduction on derivations in the strict intersection type assignment system of [2], by generalising cut-elimination, and shows a strong normalisation result for ...
Steffen van Bakel
ENTCS
2007
99views more  ENTCS 2007»
8 years 7 months ago
A Behavioural Model for Klop's Calculus
A model characterising strong normalisation for Klop’s extension of λ-calculus is presented. The main technical tools for this result are an inductive definition of strongly n...
Mariangiola Dezani-Ciancaglini, Makoto Tatsuta
CATS
2008
8 years 8 months ago
The Inhabitation Problem for Intersection Types
In the system of intersection types, without , the problem as to whether an arbitrary type has an inhabitant, has been shown to be undecidable by Urzyczyn in [10]. For one subsys...
Martin W. Bunder
CSL
2008
Springer
8 years 9 months ago
On Isomorphisms of Intersection Types
The study of type isomorphisms for different -calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms o...
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, ...
HOA
1993
8 years 11 months ago
Strong Normalization of Typeable Rewrite Systems
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 Rewri...
Steffen van Bakel, Maribel Fernández
ICFP
2000
ACM
8 years 11 months ago
Intersection types and computational effects
We show that standard formulations of intersection type systems are unsound in the presence of computational effects, and propose a solution similar to the value restriction for ...
Rowan Davies, Frank Pfenning
FOSSACS
2003
Springer
9 years 15 days ago
Type Assignment for Intersections and Unions in Call-by-Value Languages
We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functiona...
Joshua Dunfield, Frank Pfenning
TYPES
2007
Springer
9 years 1 months ago
Characterising Strongly Normalising Intuitionistic Sequent Terms
This paper gives a characterisation, via intersection types, of the strongly normalising terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the ...
José Espírito Santo, Silvia Ghilezan...
WOLLIC
2009
Springer
9 years 1 months ago
Recognizability in the Simply Typed Lambda-Calculus
Abstract. We define a notion of recognizable sets of simply typed λterms that extends the notion of recognizable sets of strings or trees. This definition is based on finite mo...
Sylvain Salvati
books