Lambda the Ultimate

VamOz: Visual Abstract Machine for Oz

VamOz is a visual abstract machine executing kernel language programs as defined in the book Concepts, Techniques and Models of Computer Programming by Peter Van Roy and Seif Haridi.

VamOz has been developed by Frej Drejhammar and Dragan Havelka with contributions from Christian Schulte. The idea is to give students a tool with which they can increase their understanding of how the abstract machine computes. VamOz has been used successfully in 2003 in the Datalogi II course taught by Christian Schulte at KTH.

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.

We are pleased to announce the Twelf Wiki, a major new source of documentation about Twelf:

http://twelf.plparty.org

Twelf is a tool used to specify, implement, and prove properties of deductive systems. The Twelf Wiki includes:

• A new introduction to LF and Twelf.
• Tutorials on common Twelf tricks and techniques.
• Case studies of larger applications of Twelf, including encodings of and proofs about linear logic, mutable state, and CPS conversion.
• Pre-compiled CVS builds of Twelf for Linux and Windows.

We invite you to come share what you know, learn from what's there, and ask questions about what's not.

- The Twelf Wiki Team

(I know many of the people working on this, and they've put in a lot of effort to make a really useful resource.)

UC Berkeley provides a webcast of the lectures for a number of their introductory college courses. Being immersed in SICP, I decided that it might be a good idea to listen to the lectures for CS 61A from Brian Harvey which uses SICP as the text. I don't know if going back to fundamentals will interest others here on LtU, but this is a good resource for a beginning CS computer course. Of course, being a series of some 40+ lectures during the course of a semester, it has both the advantages and disadvantages of learning the material through the academic setting (40+ hours is too long for casual learners).

A couple of tidbits. Although the course uses SICP as the text, it's used more as background material. The course has a certain Logo accent with the examples, with a preference for word and sentence problems rather than math problems - at least at the start of the course. It also jumps into subject matters like client-server and object-oriented programming that are a stretch of the text. Two of the lectures are occupied by videos from Alan Kay and Dan Ingalls. And the subjects of the lectures don't necessarily follow SICP in a sequential manner (the Scheme1 interpreter is interleaved with trees in chapter 2). That said, I liked seeing SICP presented from a different angle.

From a PL perspective, the most interesting piece is likely the lectures on Logo. One of the projects revolves around modifying the meta-circular evaluator to Logo. With Brian Harvey's knowledge of both Scheme (Simply Scheme) and Logo (Computer Science Logo Style), there is a lecture and a half (somewhere around the Meta-Circular subject) that goes into the parallels between Scheme and Logo. Also a discussion of the PL design decisions that went into Logo (dynamic scoping, namespace seperation,...).

(via LogBlog)

This site offers written curricular materials, based on primary historical sources, for beginning and advanced undergraduate courses in discrete mathematics and computer science. Such courses, which often cover combinatorics, deductive reasoning (logic) and algorithmic thought, draw a variety of majors, ranging from computer science, mathematics, the physical sciences and engineering to secondary education. Traditional methods of instruction follow ``The Modern American Discrete Mathematics Text,'' which although thorough and mathematically precise, present the material as a fast-paced news reel of facts and formulae, often memorized by the students, with the text itself offering only passing mention of the motivating problems and original work which eventually found resolution in modern concepts such as induction, recursion, or algorithm.

This sort of apporach is very close to my heart, as LtU readers probably know. I wish them well.

YubNub is an online command-line community extensible search engine, or as they say "a (social) command line" for the web.

Some commands which may be of interest to the community are

• ltu - Lambda-the-Ultimate.org
• scholar - Google scholar
• cs - Citeseer
• oeis - Online Encyclopedia of Integer Sequences

You can also easily create your own commands. Please share any new commands you create or find which may be relevant for the community.

[Edit: Removed "plre - Programming Language Research Engine" from the main list, since it was criticized as being self-promotional.]

As some feel that LtU is too math bound, there's only one solution for us underachievers - a Theoretical Computer Science Cheat Sheet.

(Most of it is vaguely familiar, as I've taken a lot of math courses over the years. Sadly though I'd need a much longer set of crib notes to jog my memory. Personally I think most CS based math is really simple, but it also is quite terse - much like many PLs.)

Will freshman scheming be the same if their schemes are more about robots and less about Scheme?

The MIT is going to change its curriculum structure that was famous for teaching Scheme in introductory courses. One force behind the reform is no one else than Harold Abelson, famous for his marvelous Scheme opus SICP. But why changing?

The new curriculum is designed with three goals in mind: greater flexibility in requirements, better integration of electrical engineering and computer science, and more depth to better prepare students for graduate school or real-world design challenges, he said.

And programming language wise:

Content-wise, the class is a mix as well. The first four weeks of C1 will be a lot like the first four weeks of 6.001, Abelson said. The difference is that programming will be done in Python and not Scheme.

A sign of the times?

Being a slow news week (Ehud busy, chance for shameless plug, etc...), thought I'd take the opportunity to elevate the translation of SICP to the front page. Chapter 1 is mostly complete for Alice ML/SML-NJ, Oz, Haskell, O'Caml and Scala. Still a long way from done, though portions of Chapter 2 and 3 are there for Alice ML / SML-NJ.

Actually, the more interesting item I came across this week was in a visit to the Scala list. Seems that Martin Odersky has used many examples from SICP for a course on FP - specifically the Scala by Examples document. I knew I should've made Scala a higher priority - at minimum I can borrow ideas and learn Scala along the way.

EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version. Kwangkeun Yi. JFP. 16(6):663-670.

Some 10 years ago, Harper illustrated the powerful method of proof-directed debugging for developing programs with an article in this journal. Unfortunately, his example uses both higher-order functions and continuation-passing style, which is too difficult for students in an introductory programming course. In this pearl, we present a first-order version of Harper's example and demonstrate that it is easy to transform the final version into an efficient state machine. Our new version convinces students that the approach is useful, even essential, in developing both correct and efficient programs.

The problem is regular expression matching: checking whether a string S belongs to the language specified by the regular expression r.