Lambda the Ultimate

inactiveTopic Guaranteed Optimization for Domain-Specific Programming
started 3/8/2004; 4:27:51 AM - last post 3/8/2004; 12:20:37 PM
Ehud Lamm - Guaranteed Optimization for Domain-Specific Programming  blueArrow
3/8/2004; 4:27:51 AM (reads: 8088, responses: 2)
Guaranteed Optimization for Domain-Specific Programming
T. Veldhuizen, Guaranteed Optimization for Domain-Specific Programming. In Domain-Specific Program Generation, ed. C. Lengauer and D. Batory, Lecture Notes in Computer Science, Springer-Verlag, 2003.

unless one truly needs a language with radically new semantics or syntax, it's prudent to work with a well-supported, general-purpose language (c.f. [Hud96]). Unfortunately the existing mainstream languages aren't extensible enough to do interesting, high-performance DSL work in a natural way. Therefore a fruitful direction for research is to extend the reach of general-purpose languages; in this we pursue the old, probably unattainable dream of a universal language suitable for all purposes, a dream that goes back at least to Leibniz and his grandiose vision of a Characteristica Universalis in which to formalize all human thought (c.f. [Tho01]). In the past half-century useful connections have been found between logic, type theory, algebra, compilers, and verification; perhaps it is a good time to examine these threads of convergence and take stock of the prospects for universal programming languages.

The focus of the paper is on guaranteed optimization, which addresses some aspects of performance, and proof embeddings, which address safety.

Posted to DSL by Ehud Lamm on 3/8/04; 4:29:03 AM

Mark Evans - Re: Guaranteed Optimization for Domain-Specific Programming  blueArrow
3/8/2004; 12:09:58 PM (reads: 187, responses: 1)

Worth noting: the author, Todd Veldhuizen, is primary author of the amazing Blitz++ numerics library for C++. His research overview offers an informal trace of his work to date.

Todd's paper, "Five compilation models for C++ templates," talks about the prototype Lunar compiler and "proposes an alternate structure for C++ compilers. Type analysis is removed from the compiler and replaced with a type system library which is treated as source code by the compiler."

Ehud Lamm - Re: Guaranteed Optimization for Domain-Specific Programming  blueArrow
3/8/2004; 12:20:37 PM (reads: 205, responses: 0)
Right. I was visiting his page looking for his articles about template metparogramming and expression templates in C++ when I came across this paper.