Lambda the Ultimate

The Code Generation 2009 Call for Speakers closes on Friday January 16th 2009. Accepted speakers have their conference fees waived.

Session proposals are sought covering topics such as:

• Tool and technology adoption
• Code Generation and Model Transformation tools and approaches
• Defining and implementing modelling languages
• Domain Analysis and Domain Engineering
• Language evolution and modularization
• Meta Modelling
• Runtime virtual machines versus direct code generation
• Software Product Lines and Software Factories

Visit the Code Generation 2009 web site for more information and to make a speaking submission.

Code Generation 2009 is sponsored by SoftFluent, itemis & NT/e and supported by OMG, IASA & ACCU.

Automatically Generating the Back End of a Compiler Using Declarative Machine Descriptions[PDF]
By Joao Dias

Although I have proven that the general problem is undecidable, I show how, for machines of practical interest, to generate the back end of a compiler.
...
The largest machine-dependent component in a back end is the instruction
selector. Previous work has shown that it is difficult to generate a highquality
instruction selector. But by adopting the compiler architecture developed
by Davidson and Fraser (1984), I can generate a na¨ıve instruction
selector and rely upon a machine-independent optimizer to improve the machine
instructions. Unlike previous work, my generated back ends produce
code that is as good as the code produced by hand-written back ends.

In Haskell, \f -> \g -> (((f.).).) g is equivalent to \x y z -> f (g x y z), and more generally, \f -> \g -> (((f.)... .) g with n compositions is equivalent to x1 ... xn -> f (g x1 ... xn) with n arguments.

But what is \f -> \g -> (.(.(.f))) g? Can you generalize?

What about arbitrary left and right compositions, like (.(.((.f).)))? Can a general description be given?

I am interested in your strategies in tackling such questions. I find reasoning about combinators quickly overwhelming. Sure, I can mechanically reduce a lambda term to normal form, but it's usually not that insightful. Is the key once more abstraction, through understanding of combinators at a high operational level?

Any pointers to resources for reasoning about combinators would be appreciated.

Erlang Exposed! Chris Williams from NOVAlanguages (http://tinyurl.com/9o859p) will be giving an intro to Erlang and will describe what makes it so cool. You'll learn how the Erlang Concurrency Model allows for robust multiprocessor and distributed computing. As an opening presentation, Conrad Barski will present some new software written in Arc Lisp for automated cartoon cell colorization. Afterwards, we'll head over to a Mongolian Grill for some beer and conversation.

The meeting is generously hosted by Clark & Parsia (http://tinyurl.com/6wmmbj) located at 926 N St NW REAR Studio #1 Washington DC and is near the Convention Center Metro Stop. (Map http://tinyurl.com/7mbc4o) Anyone is welcome to join our meetings!

FringeDC is a programming group in Washington DC interested in Functional and Fringe programming languages (Lisp, Haskell, Erlang, etc) http://lisperati.com/fringedc.html

I just read the PADL'03 JMatch paper (PDF), and was so impressed that I immediately downloaded JMatch and am starting to play with it.

Ehud Lamm provides a nice summary of JMatch in the LTU Classic Archives. Like him, I am surprised that JMatch didn't generate more discussion. So what do people think of JMatch today? Is there anything else like it? How does it compare to other pattern matching abstractions, e.g. F# Active Patterns?

Incidentally, any thoughts on the Polyglot Compiler Framework (used by JMatch)? Is it the framework of choice for implementing Java language extensions?

This doesnt seem to have ever made it to ltu.

http://uk.youtube.com/watch?v=yHd0u6zuWdw

The abstract:

Coconut is a developing system for high-assurance, high-performance
software. It was used to develop a library of special functions for
the Cell BE processor, which is distributed in the Cell BE SDK 3.0 as
MASS. Average performance is 4X better than the alternative
hand-tuned C library, SimdMath.

Coconut has been successful where patterns of efficient
hardware-specific computation can be captured as higher-order
functions and encoded in a Domain Specific Language embedded in
Haskell. Patterns include efficient control structures not
expressible in C, e.g., the MultiLoop, and efficient uses of SIMD
instructions which require significant compile-time computation for
pattern specialization. Some patterns interact with a novel
instruction scheduler called Explicitly Staged Software Pipelining,
based on a min-cut approach, which outperforms SWING modulo scheduling
in our tests.

A less developed aspect of Coconut is the parallel production of
proofs of correctness along with executables. Current work aims to
prove only limited properties about programs---the ones most likely to
be broken---creative use of SIMD instructions, and parallelization.
Coconut intermediate code is represented as nested code (hyper)graphs.
At the lowest level, we transform acyclic loop bodies to remove the
effect of SIMDization, and produce machine and/or human readable
specifications. This has been used to verify opaque patterns of
optimizing linear algebra for SIMD processors.

Such code graphs are embedded in higher levels containing control
flow, first single-threaded control flow optimized for ILP, and then
parallel control-flow, optimized to hide communication latency. At
this level control flow is restricted to allow peak utilization of
multi-core hardware, but enable efficient compile-time verification of
soundness. Soundness, in this context, means that the parallelized
program can be transformed into a code graph without synchronizing
control flow, because every execution can be shown to produce the same
result. Think of it as reducing the parallel debugging effort to the
single-threaded debugging problem by eliminating the non-determinism
inherent in parallel code. I will give a formal language description
of the language, and the O(n) algorithm which proves soundness and
produces the equivalent ``single threaded'' code graph.

Hi everyone,
I've been learning a small amount of type theory lately. I've noticed, as I'm sure most people have, that types in the typed lambda calculus always seem to be "determinable", I'm not sure what the correct term for it is. What I mean is this: a type is a ground type, or an arrow type, such that when applied to a term of the correct type, the type on the right of the arrow is also "determinable". For example, the following types are determinable:

Boolean (because it is a ground type)
a -> a
a -> b -> a

But these are not:
a
a -> b

Could someone point me in the right direction as to what to call this property, or if it even necessarily holds, and better yet, how to *prove* that it holds? Thanks!
-Kevin

Subject line pretty much says it all - type systems as in ML, Haskell, Scala, etc.

I've tried comp.lang.compilers and comp.lang.functional to no avail. Help me Obi Wan, you're my only hope :-)

If this is not PLT enough a topic, I'll fully understand if the moderator deletes it.

Otherwise, many, many thanks in advance.

Scott

Language extension for C/C++ for multicore-enabling performance-sensitive apps.

3 Editions (Open Source, Academic, Professional) now available.

Cilk Arts home page

Blog post re: Cilk++ for Linux

In the lambda cube, the three axes are terms-depending-on-types, types-depending-on-types and types-depending-on-types. To check my intuition:

Isn't sub-typing, in the manner of Java, C++ and C#, an example of plain terms-depending-on-types?

Are prototype-based languages, such as Javascript, plain terms-depending-on-terms?

Are multi-parameter typeclasses, C++ templates and "generics" examples of types-depending-on-types? Are associated types (for example, the iterator for a certain collection) "higher-order" or are they essentially the same thing?