Reading Group Archive (2011)
Components in Scala
On December 2 and 16 we discussed the paper Scalable Component Abstractions by Odersky and Zenger.
Monads
On November 11, we examined monadic code as a Scala state monad used in a simple partial evaluator.
On October 28 and November 4, we discussed monads as a program structuring mechanism using the comprehensive introduction Monads for functional programming by Philip Wadler.
Dart
On October 21, we discussed the new Google language Dart, particularly looking at slides from the keynote talk where it was announced and some related videos.
CoffeeScript
On October 14, we discussed the CoffeeScript language, based on the language documentation.
JavaScript
On October 7, we watched the second part of the Crockford on JavaScript video series: And Then There Was Javascript.
On September 30, we discussed the operational semantics of JavaScript based on an APLAS 2008 paper by Maffeis, Mitchell and Taly. We also watched the first video in the series Crockford on JavaScript.
Bidirectional Transformations
On September 23, Dongxi Liu from CSIRO presented a talk on the use of bidirectional transformations to process XML.
A Bidirectional XML Transformation Language for XQuery View Update
Abstract: In this talk, a bidirectional XML Transformation language will be introduced. The programs of this bidirectional language can be executed in two directions: in the forward direction, they generate materialized views from XML source data; while in the backward direction, they update the source data by reflecting back the updates on views. XQuery is a powerful functional language to query XML data. In this talk, this bidirectional language is used to interpret XQuery, such that the XML data sources and its XQuery views can be synchronized easily. Demonstrations will also be given in this talk.
Self
On September 16 we watched a video recording of a Stanford University lecture by David Ungar which is a retrospective discussion of the Self project.
Trace-based compilation
On September 2 we discussed the paper Tracing for Web 3.0: Trace Compilation for the Next Generation Web Applications by Chang at al, which discusses a novel just-in-time optimisation technique for dynamic languages.
On September 9 we discussed two follow-up papers from last week's paper on trace compilation for JavaScript:
- Trace-based just-in-time type specialization for dynamic languages by Gal et al (PLDI 2009)
- Trace-based compilation in execution environments without interpreters by Bebenita et al (PPPJ 2010)
Also, to clarify some discussion from last week, we will discuss The structure and performance of efficient interpreters by Ertl and Gregg.
Software Foundations (in Coq)
On July 29 we began a series of hands-on sessions working through Software Foundations by Pierce et al. This set of notes is an introduction to the Coq proof assistant in the context of programming languages theory. Our aim is to get to the point where attendees can use Coq to implement their own theories and proofs about them.
- August 19: the Prop: Propositions and Evidence chapter. After this date, we moved the Coq discussion to a separate group, since it is not the main focus of many of the reading group members.
- August 12: the Poly: Polymorphism and Higher-Order Functions chapter
- August 5: the remainder of the Basics chapter, and the Lists: Products, Lists and Options chapter
- July 29: read "Preface" and "Basics: Functional Programming and Reasoning About Programs", download the Software Foundations files, install Coq on a laptop, including an IDE such as Proof General or CoqIDE
Functional Pretty Printing in Scala
On July 22 Tony Sloane discussed pretty-printing in functional languages based on the paper Linear, bounded, functional pretty-printing by Swierstra and Chitil from the Journal of Functional Programming, including a discussion of implementing this approach in Scala.
System Software Verification
On June 17 and 24 Michael Olney talked us through some aspects of his efforts to prove aspects of merging in Isabelle/HOL.
On June 10 we discussed the paper Bringing Extensibility to Verified Compilers by Tatlock and Lerner from PLDI 2010.
Erlang
On May 27 Dom Verity demonstrated the main features of the Erlang programming language. It was useful to take a look at the Getting Started with Erlang Guide before the meeting.
Pluggable and Optional Type Systems
On May 20 we discussed a paper by Simon Marlow and Philip Wadler about a sub-typing system for the Erlang programming language.
On May 13 we discussed a paper by Gilad Bracha and David Griswold about StrongTalk which adds an optional type system to Smalltalk.
On May 6 we discussed pluggable type systems by looking at a position paper from Gilad Bracha as well as slides from two of his talks on this topic (talk one, talk two). Attendees also read the Lambda the Ultimate thread on this topic.
DMS Software Tool Infrastructure
On April 29 we watched a Google Tech Talk on the DMS Software Tool Infrastructure by Ira Baxter.
Growing a language
On April 15 we hosted a talk from Jose Vergara from University of Technology, Sydney about work he has been doing with Barry Jay on growing a language using pattern matching.
Abstract
This talk presents an extensible interpreter for a small language, in which each language feature, together with its parsing, typing, evaluation and printing, are isolated within a single object-oriented class. This is possible as all the necessary functionality, including string matching, queries, higher-order functions and specialised methods, can be represented by pattern-matching functions in the bondi programming language, an implementation of pattern calculus. The classes of the implementation are used to illustrate: pattern matching; integration of programming styles; language growth; and the treatment of variable binding.
Compiler Testing
On April 8 we discussed the paper Finding and Understanding Bugs in C Compilers by Xuejun Yang, Yang Chen, Eric Eide, and John Regehr (to appear at PLDI 2011). Readers may also be interested in the comment thread on this paper at Lambda the Ultimate.
Choice Calculus
On March 15 and 22 we discussed the paper The Choice Calculus: A Representation for Software Variation by Erwig and Walkingshaw (to appear in ACM TOSEM).
Version control and software variation
On March 11 we discussed the paper Operation-based merging by Ernst Lippe and Norbert van Oosterom from SDE 5 (1992).
Closure Oriented Programming Language
On March 4 Robert Smart presented his Closure Oriented Programming Language.
Abstract
Robert Smart has been trying for over 30 years to design a programming language that avoided the many annoying aspects of languages he has used. The talk will discuss his latest attempt: Closure Oriented Programming Language (COPL), giving a bit of historical context for the features. The talk will concentrate on the most recent feature of the language, the one that finally makes it all work: Behaviour Types, the types most programmers deal with, are defined by their semantics, but can have multiple inter-convertible implementations with different performance and coverage characteristics. Other features of the language include: Everything is a procedure, works similarly to "everything is an object" in some other languages; Very lightweight explicit closures are required for any optional, repeated or deferred execution; A compile time language (CTL) DSL connects the library writer to the underlying environment, removing the need for a special prefix library with mysterious powers; Super Simple Syntax allows all syntax to be user-defined syntax; Declarations by unification, with possible failure, allows case based programming style. The (optional) standard library illustrates the capabilities, and some limitations, of the language.
More information can be found here.
Paradigm-oriented software development
On Feb 18, we were delighted to host the following talk:
Title: DiaSuite: A Paradigm-Oriented Software Development Approach
Author: Charles Consel, INRIA / University of Bordeaux
We present a software development approach, whose underlying paradigm goes beyond programming. This approach offers a language-based design framework, high-level programming support, a range of verifications, and an abstraction layer over low-level technologies. Our approach is instantiated with the Sense-Compute-Control paradigm, and uniformly integrated into a suite of declarative languages and tools.
Charles Consel is a professor of Computer Science at ENSEIRB/University of Bordeaux I. He served on the faculty of Yale University, Oregon Graduate Institute and the University of Rennes. He leads the Phoenix group at INRIA. He has been designing and implementing Domain-Specific Languages (DSLs) for a variety of areas including device drivers, programmable routers, stream processing, and telephony services. These DSLs have been validated with real-sized applications and showed measurable benefits compared to applications written in general-purpose languages. His research interests include programming languages, software engineering and operating systems. (For more information, see his web page.)
Version control theory
On Feb 11, we discussed a paper that presents a formalisation of the patch theory of the Darcs revision control system.