|
|
Research Affiliation Personal Other  
|
Hi there. I've graduated and am now living in Göteborg, Sweden for a postdoc at Chalmers University of Technology. My Chalmers homepage is here, but this one is more interesting.
I am on the job market this year:
I was previously a PhD student in Computer Science at Indiana University Bloomington. My advisor was Andrew Lumsdaine and I was a member of the Open Systems Laboratory.
Here are some useful online research tools for computer science.
| Research Overview |
My dissertation, Active Libraries and
Universal Languages, is available
[PDF,
BibTeX]. Key ideas:
- We can design compilers that find optimal programs.
- These compilers have a well-defined kernel of code they will evaluate and erase at compile-time. By choosing an appropriate kernel, we can build compilers that reliably eliminate the `abstraction penalty' associated with high-level languages.
- The kernel can be used to provide staging capabilities, i.e., performing computations at compile-time to produce better run-time code. This can be used for example to perform domain-specific optimizations as is done with C++ template techniques.
- Such compilers act as complete decision procedures for a certain set of axioms. This opens an intriguing research direction of `optimizers as theorem provers' -- that is, using the optimizer to prove theorems and check proofs embedded in source code.
Thesis work: My thesis is about an optimizing compiler called Lunar aimed at high-performance and domain-specific languages. The compiler's goal is to foster the `Active Libraries' concept -- libraries that take an active role in compilation, such as providing domain-specific optimizations and safety checks.
Studying what language features are needed to realize active libraries led to the notion of languages with a Turing-complete kernel. Any programming language can be embedded into a language with a Turing-complete kernel in such a way that the embedding preserves staging (what happens at compile-time, e.g., domain-specific optimizations) and safety (compile-time safety checks). This result suggests we look to such languages for expressing domain-specific safety checks and optimizations.
Language embeddings that preserve staging and safety [PDF]
To help reach this goal, a new technique called Guaranteed Optimization has been developed so compilers can provide proven guarantees of what optimizations they will perform. Although finding optimal programs is an undecidable problem, compilers with the guaranteed optimization property find "optimal" programs within a decidable subtheory of program equivalence, using a metric that minimizes the "abstraction penalty" associated with high-level code. As well as making the behaviour of optimizing compilers more predictable, guaranteed optimization provides programmers with capabilities similar to staging and partial evaluation-- computations can be performed at compile-time to generate smarter run-time code.
- Automating Proofs of Guaranteed Optimization [PS] [PDF]
- Guaranteed optimization for domain-specific programming
(Dagstuhl No 03131) [HTML] [PS] [PDF]
- Guaranteed optimization: Proving
nullspace properties of compilers (SAS 2002, with A. Lumsdaine) [HTML] [PS] [PDF]
(Superceded by Chapter 4 of my dissertation)
The question of how to provide domain-specific safety checks got me interested in the idea of "optimizers as theorem provers." It turns out there is a close relationship between combining optimizing passes in a compiler and how theorem provers decide combinations of theories. Optimizers that perform sequences of semantic-preserving rewrites can decide combinations of equational theories in a manner similar to the Nelson-Oppen procedure. Optimizers based on superanalysis (simultaneous analyses followed by a single transformation step) can decide combinations of theories with a coinductive definition (e.g. bisimilarity). The compiler-literature notions of pessimism and optimism turn out to be induction and coinduction in disguise, and correspond to (respectively) inductive and circular proofs.
With a sufficiently powerful optimizer, it's possible to implement type systems in the language itself, an approach tentatively called embedded type systems or more generally, embedded semantics. In early work along this line I showed how the C++ template type system could be replaced by a type system library, treated as source code by the compiler. Partial evaluation is used to optimize away the type system code at compile time. This approach to compiling C++ uncouples the idea of genericity (functions which operate on arbitrary types) from the idea of specialization (duplicating functions to improve performance). When a type failure occurs, an ordinary debugger can be used to debug the type error:
Part of my thesis work requires mucking about with fixpoint equations and deciding when two systems of equations are bisimilar. Some early and important work was done on this problem in 1974 by Courcelle, Kahn and Vuillemin; their paper anticipates the modern notions of bisimilarity and term automata. Unfortunately the original paper is only in French and paper copies of the proceedings are getting scarce. I've done a translation of this paper, now provided online with the consent of B. Courcelle:
C++ Techniques and Theory: I developed some techniques useful for writing high-performance C++ libraries:
- Expression Templates
- Template Metaprograms
- C++ templates as partial evaluation (PEPM99) [HTML] [PS]
- C++ Templates are Turing Complete [PS] [PDF]
For a broad survey of performance-enhancing techniques in C++, see the technical report:
If you're a templates wonk, you might enjoy the proceedings of the 2000 and 2001 Workshops on C++ Template Programming.
Object-oriented scientific computing: I'm the primary author of the Blitz++ library, which provides numeric arrays for C++ with performance comparable to Fortran, plus many nifty features. Blitz++ performs optimizations (e.g. loop transformations) which are normally the responsibility of optimizing compilers. (The name Blitz comes from a card game I used to play as a kid that was fast and fun.) I also maintain some general resources about object-oriented numerics.
- Blitz++ Home Page
- Blitz++ User Guide [HTML] [PS]
- Arrays in Blitz++ (ISCOPE 98) [PS]
- Blitz++: The library that thinks it is a compiler (SciTools 98) [PS]
- Will C++ be faster than Fortran? (ISCOPE 97) [HTML] [PS]
- Object-Oriented Numerics Home Page
- Object-Oriented Numerics Mailing List
Grid filters and Function approximation: My MASc thesis developed a new method for approximating certain functions that arise in image restoration problems. These functions are simultaneously high-dimensional and exhibit many symmetries. The resulting filters made it possible to construct image restoration filters that can (for example) turn blurry text into crisp text. The filters are able to achieve superresolution (that is, restoring portions of a signal beyond the resolution limit of the imaging system) by learning characteristics of a signal class. Unlike polynomial- and neural network-based filters, the time cost of the filter is logarithmic in the number of coefficients.
- Grid Filters Homepage
- Grid Filters paper from ICASSP'98 [PS] [PDF]
- Grid Filters for Local Nonlinear Image Restoration (MASc Thesis) [HTML] [PS]
Computational Chinese: As a hobby, I've been building a web site waiyu.org that offers software tools for people learning CJK (Chinese/Japanese/Korean) languages. There are surprisingly fun algorithm issues: segmentation of chinese sentences into words, for example, is done with maximum log-likelihood dynamic programming. Here's an example segmentation of our lab name. The server supports proxy web browsing, so students can surf chinese web pages and get instant annotation of unfamiliar phrases. You can try this on my chinese home page, and perhaps find some off-colour jokes there; or scan the latest news from Voice of America. The main interface to the server is here.
Data mining of freeform text surveys: This software has been used to automatically analyze biographical statements of ultrarunners who compete at greater than marathon distances.
You can browse my research and related research on Google Scholar, CiteSeer or GoogleCite.
More papers, talks and articles are available here.
AKA: Todd Veldhuisen, Todd Verhuizen, Todd Velhuizen, Todd Velduizen, Todd Veldhuizer, Todd Verheusden, Todd Velduizhen, Todd Velthuizen. There is another T. Veldhuizen who studies mitten crabs and zebra mussels.
| Contact Information |
tveldhui@acm.org
Todd Veldhuizen Computing Science, Chalmers University of Technology 41296 Göteborg Sweden +46 31 772 5401