Denis Dancanet
Carnegie Mellon University
In the early eighties, Berry and Curien developed a theory
of sequential algorithms on concrete data structures, and devised
a related programming language called CDS0. Berry and Curien were trying
to solve the full abstraction problem for PCF. While they were not
successful in achieving this initial aim, their work provided the
first example of an intensional semantics. The meaning of
a PCF program can be defined to be a sequential algorithm (rather than a
continuous function on Scott domains), which allows us to
infer many of its properties: order of evaluation, computation
strategy, dependence of parts of the output on parts of the input, etc.
The game semantics, which were later used to solve the full abstraction
problem for PCF, are very closely related to sequential algorithms.
CDS0 and its theory have since provided a very fertile ground for
intensional exploration. This talk will outline some past and current
work in this area, focusing on:
- Comparison of programming languages in terms of intensional
expressiveness. Can one language express more efficient programs than
another for computing the same function?
- Circuit semantics. We define an intensional semantics which takes the
meaning of a parallel functional program to be a circuit, whose dimensions
encode its time and work complexity. This establishes a connection
with work on circuit complexity.
- Abstract interpretation and type inference. CDS0 has been used for fast
abstract interpretation of lazy higher-order functional languages.
We discuss how to use the intensional information for refinement type
inference.
We will also discuss some topics for future investigation:
- What are the benefits and drawbacks of intensional features in
a programming language? In CDS0 we can write algorithms that modify the
computation strategy of other algorithms. Is this semantics
manipulation useful? Is it the case that intensional features are
provably ``expensive'' to use?
- Is it possible to generalize sequential algorithms to model message
passing parallel languages? Can one use the intensional information
to derive interesting program properties?
For more information (papers, slides of this talk, an implementation
of CDS0 in SML/NJ), go to:
http://www.cs.cmu.edu/~ddr/my_research.html
School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213
USA
Email:dancanet@cs.cmu.edu
Home page:
http://www.cs.cmu.edu/~ddr
Back to the list of talks