Lambda the Ultimate

Interactive Tutorial of the Sequent Calculus by Edward Z. Yang.

This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic. ...

Proving theorems is not for the mathematicians anymore: with theorem provers, it's now a job for the hacker. — Martin Rinard ...

A common complaint with a formal systems like the sequent calculus is the "I clicked around and managed to prove this, but I'm not really sure what happened!" This is what Martin means by the hacker mentality: it is now possible for people to prove things, even when they don't know what they're doing. The computer will ensure that, in the end, they will have gotten it right.

The tool behind this nice tutorial is Logitext.

Kalani Thielen's The Algebra of Data, and the Calculus of Mutation is a very good explanation of ADTs, and also scratches the surfaces of Zippers:

With the spreading popularity of languages like F# and Haskell, many people are encountering the concept of an algebraic data type for the first time. When that term is produced without explanation, it almost invariably becomes a source of confusion. In what sense are data types algebraic? Is there a one-to-one correspondence between the structures of high-school algebra and the data types of Haskell? Could I create a polynomial data type? Do I have to remember the quadratic formula? Are the term-transformations of (say) differential calculus meaningful in the context of algebraic data types? Isn’t this all just a bunch of general abstract nonsense?

(hat tip to Daniel Yokomizo, who used to be an LtU member...)

From the syllabus of the Cambridge course on Usability of Programming Languages

Compiler construction is one of the basic skills of all computer scientists, and thousands of new programming, scripting and customisation languages are created every year. Yet very few of these succeed in the market, or are well regarded by their users. This course addresses the research questions underlying the success of new programmable tools. A programming language is essentially a means of communicating between humans and computers. Traditional computer science research has studied the machine end of the communications link at great length, but there is a shortage of knowledge and research methods for understanding the human end of the link. This course provides practical research skills necessary to make advances in this essential field. The skills acquired will also be valuable for students intending to pursue research in advanced HCI, or designing evaluation studies as a part of their MPhil research project.

Is this kind of HCI based research going to lead to better languages? Or more regurgitations of languages people are already comfortable with?

CRA-W/CDC and SIGPLAN Programming Languages Mentoring Workshop, Philadelphia, PA (co-located with POPL 2012) Tuesday January 24, 2012

We are pleased to invite students interested in programming languages research to the first PL mentoring workshop. The goal of this workshop is to introduce senior undergraduate and early graduate students to research topics in programming language theory as well as provide career mentoring advice to help them get through graduate school, land a great job, and succeed. We have recruited leaders from the programming language community to provide overviews of current research topics, and have organized panels of speakers to give students valuable advice about how to thrive in graduate school, search for a job, and cultivate habits and skills that will help them in research careers.

This workshop is part of the activities surrounding POPL, the Symposium on Principles of Programming Languages, and takes place the day before the main conference. One goal of the workshop is to make the POPL conference more accessible to newcomers and we hope that participants will stay through the entire conference.

Through the generous donation of our sponsors, we are able to provide travel scholarships to fund student participation. These travel scholarships will cover reasonable travel expenses (airfare, hotel and registration fees) for attendance at both the workshop and the POPL conference. Anyone may apply for a travel scholarship, but first priority will be given to women and under-represented minority applicants.

The workshop registration is open to all. Students with alternative sources of funding for their travel and registration fees are welcome.

APPLICATION FOR TRAVEL SUPPORT:
The travel funding application can be accessed from the workshop web site. The deadline for full consideration of funding is December 2, 2011. Selected participants will be notified starting December 9th and will need to register for the workshop by December 24th.

ORGANIZERS:
Stephanie Weirich, Kathleen Fisher and Ron Garcia

SPONSORS:
The Computing Research Association's Committee on the Status of Women (CRA-W), the Coalition to Diversify Computing (CDC), and the ACM Special Interest Group on Programming Languages (SIGPLAN).

We don't usually post conference or workshop announcements on the front page, but this seemed sufficiently new and worthy to me. Please note that the deadline for the application for travel support is only two days away!

Programming and Scaling, a one-hour lecture by Alan Kay at his finest (and that's saying something!)

Some of my favorite quotes:

• "The biggest problem we have as human beings is that we confuse our beliefs with reality."
• "We could imagine taking the internet as a model for doing software modules. Why don't people do it?" (~00:17)
• "One of the mistakes that we made years ago is that we made objects too small." (~00:26)
• "Knowledge in many cases trumps IQ. [Henry] Ford was powerful because Isaac Newton changed the way we think." (~00:28)
• "Knowledge is silver. Outlook is gold. IQ is a lead weight." (~00:30)
• "Whatever we [in computing] do is more like what the Egyptians did. Building pyramids, piling things on top of each other."
• "The ability to make science and engineering harmonize with each other - there's no greater music." (~00:47)

And there are some other nice ideas in there: "Model-T-Shirt Programming" - software the definition of which fits on a T-shirt. And imagining source code sizes in terms of books: 20,000 LOC = a 400-page book. A million LOC = a stack of books one meter high. (Windows Vista: a 140m stack of books.)

Note: this a Flash video, other formats are available.

Andrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml.

If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out.

It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more hands-on way to get to grips with CBPV would be to implement any of these missing features.

The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here.

Is Transactional Programming Actually Easier?, WDDD '09, Christopher J. Rossbach, Owen S. Hofmann, and Emmett Witchel.

Chip multi-processors (CMPs) have become ubiquitous, while tools that ease concurrent programming have not. The promise of increased performance for all applications through ever more parallel hardware requires good tools for concurrent programming, especially for average programmers. Transactional memory (TM) has enjoyed recent interest as a tool that can help programmers program concurrently.

The TM research community claims that programming with transactional memory is easier than alternatives (like locks), but evidence is scant. In this paper, we describe a user-study in which 147 undergraduate students in an operating systems course implemented the same programs using coarse and fine-grain locks, monitors, and transactions. We surveyed the students after the assignment, and examined their code to determine the types and frequency of programming errors for each synchronization technique. Inexperienced programmers found baroque syntax a barrier to entry for transactional programming. On average, subjective evaluation showed that students found transactions harder to use than coarse-grain locks, but slightly easier to use than fine-grained locks. Detailed examination of synchronization errors in the students’ code tells a rather different story. Overwhelmingly, the number and types of programming errors the students made was much lower for transactions than for locks. On a similar programming problem, over 70% of students made errors with fine-grained locking, while less than 10% made errors with transactions.

I've recently discovered the Workshop on Duplicating, Deconstructing, and Debunking (WDDD) and have found a handful of neat papers, and this one seemed especially relevant to LtU.

[Edit: Apparently, there is a PPoPP'10 version of this paper with 237 undergraduate students.]

Also, previously on LtU:

Transactional Memory versus Locks - A Comparative Case Study

Despite the fact Tommy McGuire's post mentions Dr. Victor Pankratius's talk was at UT-Austin and the authors of this WDDD'09 paper represent UT-Austin, these are two independent case studies with different programming assignments. The difference in assignments is interesting because it may indicate some statistical noise associated with problem domain complexity (as perceived by the test subjects) and could account for differences between the two studies.

Everyone always likes to talk about usability in programming languages without trying to do it. Some claim it can't even be done, despite the fact Horning and Gannon did work on the subject 3+ decades ago, assessing how one can Language Design to Enhance Program Reliability. This gives a glimpse both on (a) why it is hard (b) how you can still try to do usability testing, rather than determine the truthiness of a language design decision.

Matthew Might, "Abstract interpreters for free", Static Analysis Symposium 2010 (SAS 2010).

...we present a two-step method to convert a small-step concrete semantics into a family of sound, computable abstract interpretations. The first step re-factors the concrete state-space to eliminate recursive structure; this refactoring of the state-space simultaneously determines a store-passing-style transformation on the underlying concrete semantics. The second step uses inference rules to generate an abstract state-space and a Galois connection simultaneously. The Galois connection allows the calculation of the “optimal” abstract interpretation. The two-step process is unambiguous, but nondeterministic: at each step, analysis designers face choices. Some of these choices ultimately influence properties such as flow-, field- and context-sensitivity. Thus, under the method, we can give the emergence of these properties a graph-theoretic characterization.

The work in this paper provides some context for known static analysis techniques like k-CFA, and also opens up some interesting new directions for static analysis development. Also, as Matt points out, there are some pedagogical benefits to having a systematic process for getting from semantics to abstract interpretation.

Why Undergraduates Should Learn the Principles of Programming Languages

The linked document is the first public release of a document discussing the value of programming languages principles for undergraduate CS majors. The intended audience is computer scientists who are not specialists in programming languages. Please leave comments on how well you believe it meets its goals and with suggestions for improvements.

Abstract: Undergraduate students obtain important knowledge and skills by studying the pragmatics of programming in multiple languages and the principles underlying programming language design and implementation. These topics strengthen students' grasp of the power of computation, help students choose the most appropriate programming model and language for a given problem, and improve their design skills. Understanding programming languages thus helps students in ways vital to many career paths and interests.

It would be nice if people interested in this as much as Kim Bruce could actively post such stuff to LtU as contributing editors, hint hint professors...

Edit: In case Kim Bruce is listening, I found this link today via Hacker News posting. There are some comments there, too.

Maxine VM is an open source meta-circular JVM from Sun.

Maxine is a VM designed for and written in the Java(TM) Programming Language with an emphasis on leveraging meta-circularity, componentized design, and code reuse to achieve flexibility, configurability, and productivity for academic and industrial virtual machine researchers.

The Maxine Inspector [5min, YouTube] seems pretty neat! Bringing VM research to the masses :)
A longer presentation by Bernd Mathiske at the JVM Language Summit 2008 provides a good introduction.