Lambda the Ultimate

It seems to me that LtU has many new readers and contributors since moving to the new site. That's great!

Yet it seems to me that the situation right now is that LtU has readers with very different backgrounds, among them many readers who haven't studied PL formally. Others come from academia, and study PL theory for a living.

Since we have such a lively community it occured to me to start a thread for advice on where to begin aimed at those who haven't studied PL theory, yet want to follow the papers and books we discuss.

So the question, mostly directed at old timers, is to which resources would you send a friend asking for advice on learning about the theoretical study of programming languages?

P.S The early LtU archives may be helpful, since I used LtU to organize and collect the papers I read when I began my studies in the field.

To coincide with the reprinting of Principles of Program Analysis by Flemming Nielson, Hanne Riis Nielson and Chris Hankin the authors launched a new web page containing lecture slides and other supplementary material.

The lecture slides cover things like data flow analysis, control flow analysis and abstract interpretation.

An critique of OOP. The article is about OOP as a SE/design approach and doesn't directly attack the issue from a PL angle, but it might still interest LtU readers.

From a PL point of view, I would have chnaged the title to: OOP Is Much Better in Theory Than in Practice, (And the Theory Isn't too Good anyway).

Getting sick of Python posts by now? Sorry...

A large part of this presentation consists of a series of code examples showing how something is done in pure Java versus a Jython version. A nice illustration of the differences between the languages (did anyone say explicit static typing?) and about their different abstraction facilities and domain specific abstractions (e.g., builtin dictionaries and list comprehensions).

Analyzing these examples may be fun exercise idea for those of us teaching PL courses.

Oleg's presentation at the workshop in honor of Daniel Friedman is great fun as usual. The topic of repeated applications of call/cc has been mentioned on LtU previously, a few years ago. New this time: the full and correct beta-normalizer written as a direct-style syntax-rule. The normalizer implements calculus of explicit substitutions. The talk presents probably the shortest (and the fastest) normal-order beta-normalizer as a (stand-alone) Scheme macro. Another new feature is the discussion of self-applications of delimited continuation operators. The talk mentions incidentally that shift, control, shift0 and other, less-delimited control operators are the members of the same family: gshift/greset.

Hot stuff.

I guess the record wouldn't be complete without mentioning this proposal,

This PEP proposes an extension to "duck typing" called "monkey typing", that preserves most of the benefits of duck typing, while adding new features to enhance inter-library and inter-framework compatibility. The name comes from the saying, "Monkey see, monkey do", because monkey typing works by stating how one object type may mimic specific behaviors of another object type.

More here and here (from Guido).

The long awaited sequel to Types and Programming Languages by Benjamin Pierce is out! Check it out here:
Advanced Topics in Types and Programming Languages.

It is available from amazon. I'm certainly getting a copy. TAPL was great!

A discussion with some interesting views and perspective.

Here you'll find code snipptes showing the API of the various libraries (all of them used to solve the same programming task), and comments about the behaviour of each of the libraries.

I am not sure if this item should be categorized as being pro-libraries, pro-a big standard libary, or pro-builtin language support for XML.

You decide.

It's widely appreciated that knowing that a distributed system or protocol behaves correctly is generally hard, and that process algebras provide useful formalisms for reasoning about these. Less appreciated is how hard it is to turn informal correctness proofs into formal proofs using process algebras.

Process algebra needs proof methodology (Fokkink, Groote & Reniers), an introductory article published a year ago in the Bulletin of the EATCS, provides a nice introduction to the problem of making process algebras more tractable for correctness reasoning, using Tanenbaum's sliding window protocol as a running example of a surprisingly hard-to-formalise proof.

Perhaps as interesting for LtU readers is that the article comes from the negelected "third" approach to process algebra (after CCS and CSP), namely the Algebra of Communicating Processes of Bergstra and Klop.

Under the category of "what I'm up to", found the book by Milner and Tofte at the used bookstore over the weekend. On chapter 8 at the moment. I see that the Commentary book is online for those who haven't read it yet (last published in 1991, it's out of print).

This book is the companion to the Definition of Standard ML, which defines SML in mathematical terms. The Commentary is a bit more approachable, but I must admit that I probably could use a "Commentary on the Commentary on Standard ML", to make the Commentary digestable. But then the two books are aimed at implementors of the language. Still, I managed to pick up some useful information on ML here and there.