| Date | Speaker | Title (click for abstract) | Location |
| Feb. 23, 2006 | Karl Trygve Kalleberg | Stratego/XT in a Nutshell -- An introduction to the Stratego/XT transformation system | DC 1316 |
| Mar. 02, 2006 | Brad Lushman | The R-Acyclic Semiunification Problem | DC 1304 |
| Mar. 09, 2006 | Ondřej Lhoták | Context-sensitive points-to analysis: is it worth it? | DC 1331 |
| Mar. 16, 2006 | no talk | no talk | |
| Mar. 23, 2006 | Yuan Lin | An Algebraic Foundation for Name Resolution in C-like Languages | DC 1302 |
| Mar. 30, 2006 | no talk | no talk | |
| Apr. 06, 2006 | CANCELLED | CANCELLED | CANCELLED |
| Apr. 13, 2006 | no talk | no talk | |
| Apr. 20, 2006 | David Yeung | An Introduction to Quantum Programming Languages | DC 1331 |
| Apr. 27, 2006 | no talk | no talk |
Seminars are Thursdays at 2:30 pm, unless otherwise indicated.
All are welcome.
Talk announcements are also posted to a public mailing list.
To volunteer to give a talk, contact Ondřej Lhoták. Talks can range from informal to formal, and they can be about any of the following:
The purpose is for us all to see what people are interested in, and motivate discussions.
I will show how Stratego and XT together are used to implement
JavaSWUL, a language extension to Java for writing user
interfaces, and also mention how the system has been applied
to tasks such as compilation, optimization, reengineering, and
program verification.
The R-Acyclic Semiunification Problem
Brad Lushman
Mar. 02, 2006
The semiunification problem (SUP) is an undecidable problem whose connections
to the type systems of certain languages has led to proofs of undecidable type
inference. On the other hand, the acyclic semiunification problem (ASUP) is a
decidable subset of SUP whose decidability has made type inference for
restricted type systems within these languages possible. The acyclicity
condition that defines ASUP is phrased in terms of the existence of a
particular kind of partition of the variables in the problem instance into
pairwise disjoint sets. In this talk, we rephrase the acyclicity restriction
of ASUP in graph-theoretic terms. Under this new view of the problem, we show
how the acyclicity condition for ASUP can be relaxed, without sacrificing
decidability. The result is a larger decidable subset of SUP, which we call
the R-acyclic semiunification problem (R-ASUP). An immediate consequence of
the decidability of R-ASUP is a more concise formulation of a known typing
algorithm.
Context-sensitive points-to analysis: is it worth it?
Ondřej Lhoták
Mar. 09, 2006
Joint work with Laurie Hendren, McGill University.
We present the results of an empirical study evaluating the precision of subset-based points-to analysis with several variations of context sensitivity on Java benchmarks of significant size. We compare the use of call site strings as the context abstraction, object sensitivity, and the BDD-based context-sensitive algorithm proposed by Zhu and Calman, and by Whaley and Lam. Our study includes analyses that context-sensitively specialize only pointer variables, as well as ones that also specialize the heap abstraction. We measure both characteristics of the points-to sets themselves, as well as effects on the precision of client analyses. To guide development of efficient analysis implementations, we measure the number of contexts, the number of distinct contexts, and the number of distinct points-to sets that arise with each context sensitivity variation. To evaluate precision, we measure the size of the call graph in terms of methods and edges, the number of devirtualizable call sites, and the number of casts statically provable to be safe.
The results of our study indicate that object-sensitive analysis
implementations are likely to scale better and more predictably than the
other approaches; that object-sensitive analyses are more precise than
comparable variations of the other approaches; that specializing the
heap abstraction improves precision more than extending the length of
context strings; and that the profusion of cycles in Java call graphs
severely reduces precision of analyses that forsake context sensitivity
in cyclic regions.
An Algebraic Foundation for Name Resolution in C-like Languages
Yuan Lin
Mar. 23, 2006
Names (identifiers) and their usage contain critical semantic
information about software. It follows that name resolution is important
in fields of computer science that analyze or modify software, including
compiler construction, program comprehension and program transformation.
Traditionally, the rules that define name resolution have been informal
and their implementations tend to be time consuming and error prone. This
paper gives an approach such that name resolution can be specified
formally and can be automatically implemented based on the specification.
We present binary relational algebra as a foundation for name resolution.
In our approach, we represent the key facts about software as binary
relations and we translate traditional language specifications for name
resolution into binary relational algebraic formulas. Using this
approach, we can neatly and concisely specify name resolution for C-like
languages such as C, the C Preprocessor and Java. We base these
specifications on four algebraic formulas, which we call the Category,
Name, Visibility and Priority Rules. Our specifications can be efficiently
executed by existing languages or databases that implement relational
algebra. Since these specifications are in a formal notation, they can be
verified.
Our research indicates that binary relational algebra is expressive enough
to model name resolution in C-like languages. It also implies that
existing software tools, including relational database systems, can
resolve names in these languages. To validate the application of our
research in practice, we applied our approach to name resolution to open
source programs and found that the execution times are satisfactory.
An Introduction to Quantum Programming Languages
David Yeung
Apr. 20, 2006
In the early quantum computation literature, algorithms were often
expressed in an ad hoc manner using low-level specifications (such
as circuit diagrams or Turing machines) accompanied by a meta-level
description of the high-level control flow. Researchers soon
realized, as in the case of classical computer programs, that
there were a number of benefits to writing quantum algorithms
in a high-level programming language. A program written in such a
language captures both the data flow and the control flow of an
algorithm. A high-level programming language also provides a number
of additional benefits over the traditional ad hoc descriptions:
structured data types, control flow operations such as loops
and subroutines, a degree of portability and hardware independence,
etc. When the classical and quantum parts of an algorithm are
expressed in the same language, it also becomes possible to
simulate the algorithm without the use of quantum hardware.
In this talk, I will give a brief introduction to the field of quantum programming languages. I will outline and discuss some of the differences between classical programming languages and quantum ones, and address some of the issues that arise in the design of the latter. The talk is aimed at programming language researchers and does not assume a background knowledge of quantum computation.