[Prev][Next][Index][Thread]
Special Issue of Mathematical Structures in Computer Science
-- Special Issue of Mathematical Structures in Computer Science on
Intersections Types and Applications --
edited by M.Dezani and S.Ronchi
IMPORTANT DATE:
Submission of papers: December 31, 2000
SCOPE AND OBJECTIVES:
Intersection types were introduced roughly twenty years ago to provide
type polymorphism by listing type instances. This differs from the more
widely used universal types, which provide type polymorphism by giving a
type scheme that can be instantiated into various type instances. In
particular, intersection types polymorphism is stronger than universal
polymorphism, as far as the typability power is concerned. (A similar
relationship holds between union types and existential types, the duals
of intersection types and universal types.)
Since the very beginning, intersection types have been used as a
powerful tool both for the analysis and the synthesis of lambda models.
On one hand, intersection types disciplines provide finitary inductive
definitions of interpretations of lambda terms in models. On the other
hand, they are suggestive for the shape the domain model has to have in
order to exhibit desired properties.
There has been a great amount of theoretical research on intersection
types over the last twenty years.
Recently, intersection types (and similar technology) have been
increasingly used for practical purposes as well.
Aim of this special issue is to collect papers on the more recent
developments of studies about intersection types, both from a
theoretical and an applicative point of view.
TOPICS FOR SUBMITTED PAPERS:
Possible topics for submitted papers include, but are not limited to:
* Applications to the description of operational and denotational
properties of lambda calculi and functional languages.
* Applications to the analysis and the synthesis of domains for
denotational semantics.
* Results on formal properties: principal typings, normalization
properties (for normal forms, head-normal forms, weak head-normal forms,
etc.), type inference algorithms, etc.
* Results for clearly related systems, e.g., systems with union types,
refinement types, or singleton types.
* Connections with not-so-clearly related approaches such as abstract
interpretation and constraints.
* Applications for programming languages, e.g., program analysis (flow,
strictness, totality, etc.), accurate type error messages, increased
flexibility with static typing, separate compilation, optimizing
transformations, types for objects, etc.
* Applications for other areas, e.g., database query languages, program
extraction from proofs, type systems for natural languages.
SUBMISSION INSTRUCTIONS:
The papers must be of very high quality reflecting a new emphasis upon
the use of mathematical concepts and results in Computer Science,
broadly construed.
They will be referred as standard submissions to Mathematical Structures
in Computer Science.
Accepted papers must be typed using the Mathematical Structures in
Computer Science LaTeX style.