Lambda the Ultimate

To quote Richard Zach:

CSLI Lecture Notes are now part of the Stanford Medieval and Modern Thought Digitization Project. That means books such as Unger's Cut-elimination, Normalization, and the Theory of Proofs, Troelstra's Lectures on Linear Logic, Aczel's Non-well-founded Sets, van Benthem's Manual of Intensional Logic, and Goldblatt's Logics of Time and Computation are now available online and for free. (HT: Shawn)

Also of interest here will be McCarthy's Defending AI research, and Modal logic and process algebra : a bisimulation perspective, edited by Venema, de Rijke and Ponse.

Leo Brodie's books Thinking Forth and Starting Forth are now available for download and the first is back in print. This material had been hard to find for a long time!

Shriram Krishnamurthi's excellent book, Programming Languages: Application and Interpretation (PLAI), long available in PDF form, is now available in paperback.

There's also a paid download available, "in case you want to reward the author in kind". A free PDF of the latest version is still available, which "really is the entire book, with no strings attached." The book is now licensed under a Creative Commons license which allows it to be adapted ("remixed") to fit a course.

Here's an overview of the book's approach:

This book unites two approaches to teaching programming languages, one based on a survey of languages and the other on writing definitional interpreters.

Each approach has significant advantages but also huge drawbacks. The interpreter method writes programs to learn concepts, and has at its heart the fundamental belief that by teaching the computer to execute a concept we more thoroughly learn it ourselves. While this reasoning is internally consistent, it fails to recognize that understanding definitions does not imply we understand the consequences of those definitions. For instance, the difference between strict and lazy evaluation, or between static and dynamic scope, is only a few lines of interpreter code, but the consequences of these choices is enormous. The survey of languages school is better suited to understand these consequences.

The book is used as the textbook for the programming languages course at Brown University, taken primarily by 3rd and 4th year undergraduates and beginning graduate (both MS and PhD) students. It seems very accessible to smart 2nd year students too. The book has been used as a textbook at over a dozen other universities as a primary or secondary text.

When published, this collection of essays edited by Greg Wilson and Andy Oram will likely be of interest to LtU readers.

Among the contributors are Brian Kernighan, Simon Peyton Jones (whose contribution we already discussed) and Kent Dybvig.

Take a look at the ToC and let us know which essay titles intrigue you the most...

This will be of interest to LtU readers in India and maybe for others as well.

I just noticed the existence of this O'Reilly book penned, so it seems, by Maurice Naftalin and (believe it or not) Philip Wadler! Is this for real, or a very elaborate hoax? It seems possible, if you remember the history of Java generics, so I guess it's true, but if someone actually saw a copy I'd be reassured...

The blurb, by the way, is from Gilad Bracha who says that this is a crystal-clear tutorial that starts with the basics and ends leaving the reader with a deep understanding of both the use and design of generics. Ya think?!

Practical OCaml. Joshua Smith.

Apress has recently published a "mainstream" book (in English!) on OCaml. Here is an interview with the author, on a Ruby blog, of all places. I haven't seen the book yet, but will certainly buy it. If it's as good as Practical Common Lisp and generates as much buzz, this will be a very nice thing.

This whole book by Ulrich Breymann is online (I don't think I've seen this mentioned here before).

Probably would have posted this to the previous LtU story on The Reasoned Schemer, but since Ehud requested that we post some (cool) stories...

As I've mentioned in a couple of posts, I've been working on an Oz Translation of the example code in the book. At this juncture, I've got large chunks of the first seven chapters translated. It probably shouldn't be surprising that the logic programming in miniKANREN and Oz are eerily similar, given that both have been influenced by Prolog (and also given the fact that great minds think alike). Because I spent more time on the example in 3.10-3.13 then all the others combined, I think it useful in seeing the parallel. In miniKANREN, we have:

(define listo
  (lambda (l)
    (conde
      ((nullo l) succeed)
      ((pairo l)
       (fresh (d)
         (cdro l d)
         (listo d)))
      (else fail))))

(run 5 (x)
 (listo `(a b c . ,x)))

For the same examples, we have the Oz code of:

fun {Listo L}
   choice
      L = nil
   [] H T in
      L = H|T
      H|{Listo T}
   end
end

{SolveN 5 
   fun {$} X in 
      _ = {Listo a|b|c|X} 
      X
   end}

From this code, I've concluded that "run" translates to "Solve" and that "conde" corresponds to "choice". Some may find the correlation of the languages to be useful in working their way through the book, being able to tap into another way of expressing the ideas. The main difference between the two languages has to do with the various alternative search strategies. "conde" specifies a depth-first search strategy, while "condi" is a breadth-first strategy. The all, alli, conda, and condu are other variations on strategies. While Oz gives one a lot of flexibility to vary the search strategy for computation spaces, the actual strategy is determined by the Solve function (which corresponds to the "run" function in Scheme), not in the declaration of choice (conde, condi, conda, condu).

Although the other search strategies can be programmed in Oz, I'm not expert enough at this point to modify the Solve function. The remainder of the translation will have to wait until I get edumacated, or someone else completes the thought.

A new release of Shriram Krishnamurthi's programming languages book is available.