Teaching & Learning
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.
I owe Martin Odersky and his team at EPFL an apology: as you can see, I'm posting this rather dramatically late, as the deadline for submission has already passed. Nevertheless, hopefully the notice of the event itself is still worthwhile.
The First Scala Workshop
Call for Papers
Scala is a general purpose programming language designed to express
common programming patterns in a concise, elegant, and type-safe
way. It smoothly integrates features of object-oriented and
This workshop is a forum for researchers and practitioners to share
new ideas and results of interest to the Scala community. The first
workshop will be held at EPFL in Lausanne, Switzerland, on Thursday
15 April 2010, co-located with Scala Days 2010 (15-16 April).
We seek papers on topics related to Scala, including (but not
1. Language design and implementation -- language extensions,
optimization, and performance evaluation.
2. Library design and implementation patterns for extending Scala --
embedded domain-specific languages, combining language features,
generic and meta-programming.
3.Formal techniques for Scala-like programs -- formalizations of the
language, type system, and semantics, formalizing proposed language
extensions and variants, dependent object types, type and effect
4. Concurrent and distributed programming -- libraries, frameworks,
language extensions, programming paradigms: (Actors, STM, ...),
performance evaluation, experimental results.
5. Safety and reliability -- pluggable type systems, contracts,
static analysis and verification, runtime monitoring.
6. Tools -- development environments, debuggers, refactoring
tools, testing frameworks.
7. Case studies, experience reports, and pearls
Submission: Friday, Jan 15, 2010 (24:00 in Apia, Samoa)
Notification: Monday, Feb 15, 2010
Final revision: Monday, Mar 15, 2010
Workshop: Thursday, Apr 15, 2010
Submitted papers should describe new ideas, experimental results, or
projects related to Scala. In order to encourage lively discussion,
submitted papers may describe work in progress. All papers will be
judged on a combination of correctness, significance, novelty,
clarity, and interest to the community.
Submissions must be in English and at most 12 pages total length in
the standard ACM SIGPLAN two-column conference format (10pt).
No formal proceedings will be published, but there will be a webpage
linking to all accepted papers. The workshop also welcomes short papers.
Submission instructions will be published at:
Ian Clarke, Uprizer Labs
William Cook, UT Austin
Adriaan Moors, KU Leuven
Martin Odersky, EPFL (chair)
Kunle Olukotun, Stanford University
David Pollak, Liftweb
Lex Spoon, Google
Certified Programming With Dependent Types
From the introduction:
We would all like to have programs check that our programs are correct. Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits. The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science. Beyond the convincing, I also want to provide a handbook on practical engineering of certified programs with the Coq proof assistant.
This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights.
Please note that Adam is explicitly requesting feedback on this work.
Mitchel Resnick, John Maloney, Andrés Monroy Hernández, Natalie Rusk, Evelyn Eastmond, Karen Brennan, Amon Millner, Eric Rosenbaum, Jay Silver, Brian Silverman, Yasmin Kafai, Scratch: Programming for All, Communications of the ACM, vol. 52, no. 11, November 2009.
When Moshe Vardi, Editor-in-Chief of CACM, invited us to submit an article about
Scratch, he shared the story of how he learned about Scratch:
A couple of days ago, a colleague of mine (CS faculty) told me how she tried to
get her 10-year-old daughter interested in programming, and the only thing that
appealed to her daughter (hugely) was Scratch.
That’s what we were hoping for when we set out to develop Scratch six years ago. We
wanted to develop an approach to programming that would appeal to people who hadn’t
previously imagined themselves as programmers. We wanted to make it easy for
everyone, of all ages, backgrounds, and interests, to program their own interactive stories,
games, animations, and simulations – and to share their creations with one another.
Scratch is the cover story of the November 2009 issue of CACM. The goal of Scratch is to get kids programming so that they become more fluent in information technology, and develop "computational thinking" skills. Scratch is a graphical language based on a collection of “programming blocks” that children snap together like Lego blocks to create programs. The programs themselves appear to be imperative in nature (at least based on the samples in the CACM article). Programs can be made concurrent by creating multiple stacks of blocks, and the authors claim that their goal is to make concurrent execution as intuitive as parallel execution.
Scratch was previously mentioned on LtU here.
A survey about state of the art C compiler optimization tricks, Felix von Leitner, Linux Kongress 2009.
The introduction and the conclusion is quite well put:
- If you do an optimization, test it on real world data.
- If it’s not drastically faster but makes the code less readable: undo it.
That's certainly something that I agree with 110%. And really, that's why a good compilers course is so important, even if the vast majority of students never write a compiler outside of class.
Safe Garbage Collection = Regions + Intensional Type Analysis, by Daniel C. Wang and Andrew W. Appel:
We present a technique to implement type-safe garbage collectors by combining existing type systems used for compiling type-safe languages. We adapt the type systems used in region inference  and intensional type analysis  to construct a safe stop-and-copy garbage collector for higher-order polymorphic languages. Rather than using region inference as the primary method of storage management, we show how it can be used to implement a garbage collector which is provably safe. We also introduce a new region calculus with non-nested object lifetimes which is signiﬁcantly simpler than previous calculi. Our approach also formalizes more of the interface between garbage collectors and code generators. The efﬁciency of our safe collectors are algorithmically competitive with unsafe collectors.
I'm surprised this region calculus hasn't received more attention or follow-up discussion in subsequent papers. It seems eminently practical, as it replaces the more complicated alias analyses required in other region calculi, with garbage collection of region handles; seems like a huge improvement over general GC, assuming region inference is sufficiently precise.
Verified Programming in Guru is a tutorial introduction to Guru:
GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs.
In comparison to Coq:
GURU is inspired largely by the COQ theorem prover, used for formalized mathematics and theoretical computer science, as well as program verification. Like COQ, GURU has syntax for both proofs and programs, and supports dependent types. GURU does not have as complex forms of polymorphism and dependent types as COQ does. But GURU supports some features that are difficult or impossible for COQ to support, which are useful for practical program verification. In COQ, the compiler must be able to confirm that all programs are uniformly terminating: they must terminate on all possible inputs. We know from basic recursion theory or theoretical computer science that this means there are some programs which really do terminate on all inputs that the compiler will not be able to confirm do so. Furthermore, some programs, like web servers or operating systems, are not intended to terminate. So that is a significant limitation. Other features GURU has that COQ lacks include support for functional modeling of non-functional constructs like destructive updates of data structures and arrays; and better support for proving properties of dependently typed functions.
The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen.
A Functional I/O System (or Fun for Freshman Kids), by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. ICFP 2009.
Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics.
We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa) -- just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.
This is a paper explaining some of the technical underpinnings of the How to Design Worlds curriculum that the PLT group has worked on.
I was tempted to categorize this as "functional", but decided against it. One of the really nice features of this curriculum is actually its applicability to imperative programming. Here, students are taught to think of interactive programs as functions written in world-passing style, and to specify programs in terms of the invariants that the function maintains on the world data.
That is: students are taught about loop invariants, without ever having to write an explicit loop. In my experience, loop invariants are the most difficult part of explaining Hoare logic (and hence of explaining imperative programming), because they require imagining a dynamic picture of what the static source code will eventually do. This style of teaching helps to manage that difficulty by making the dynamic state into visible animations.