PL Reading Group Archive

This page lists the past topics of the Programming Languages and Verification Reading Group.

Note: topics are listed in reverse chronological order.

Topics from 2018 

Incremental Parsing


On November 16, Cameron Pappas presented his COMP796 project that developed an implementation of incremental parsing in the Rats! parser generator, based on the paper “Incremental packrat parsing” by Dubroy and Warth from the 2017 Software Language Engineering conference.


 On October 12 we looked at the Observable JavaScript notebook platform. Compared to other notebook systems such as Jupyter, the Observable platform is notable because it automatically re-evaluates cells based on dependencies, which removes ordering and re-evaluation errors.

 The State of Fault Injection Vulnerability Detection

On September 28, Thomas Given-Wilson presented his work described below.

 Fault injection is a well known method to test the robustness and security vulnerabilities of software. Fault injections can be explored by simulations (cheap, but not validated) and hardware experiments (true, but very expensive). Recent simulation works have started to apply formal methods to the detection, analysis, and prevention of fault injection attacks to address verifiability. However, these approaches are ad-hoc and extremely limited in architecture, fault model, and breadth of application. Further, there is very limited connection between simulation results and hardware experiments. Recent work has started to consider broad spectrum simulation approaches that can cover many fault models and relatively large programs. Similarly the connection between these broad spectrum simulations and hardware experiments is being validated to bridge the gap between the two approaches. This presentation highlights the latest developments in applying formal methods to fault injection vulnerability detection, and validating software and hardware results with one another.

Thomas Given-Wilson is a post-doctoral researcher at INRIA TAMIS, Le Chesnay, France. He holds a PhD from the University of Technology, Sydney.

Control-flow Reconstruction

On September 14, Dominik Klumpp will present his work described below.

Control Flow Reconstruction for Binary Programs: A Trace Abstraction Refinement-Based Method

Binary code is a low-level machine code representation of programs that can be directly executed by a processor. Due to its low-level nature, it is well-suited for high-precision analyses of qualitative and quantitative properties (such as worst case execution time).However, establishing such properties of binary code is notoriously hard, because the code is unstructured and can contain indirect jumps (gotos) whose target address is dynamically calculated at runtime. As a result, standard software analysis techniques that rely on the availability of the control flow graph (CFG) of a program cannot be directly applied to the analysis of binary code.

In this talk, we address the problem of constructing CFGs for binary programs. We present a novel technique based on trace abstraction refinement, and demonstrate that our technique constructs CFGs satisfying several formally-defined quality criteria.

Dominik Klumpp is a student in the joint MSc. Software Engineering course at the University of Augsburg, the Technical University Munich and the Ludwig-Maximilians-University Munich. He is currently visiting at Macquarie University for his master thesis on control flow reconstruction for binary programs.

On September 7 we discussed the paper “An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries” by Kinder et al from VMCAI 2009.

Effect-based Languages

On August 31 we discussed the paper “Programming and reasoning with algebraic effects and dependent types” by Edwin Brady from ICFP 2013 (

On August 17 and 24 we discussed the paper "Do be do be do" by Lindley et al from POPL 2017 (updated version arXiv) that defines and illustrates the Frank programming language.

Automated Software Verification

On July 27 we discussed the paper "Invariant Synthesis for Combined Theories" by Beyer et al.

On June 29 we discussed the paper From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis by Harman and O'Hearn from SCAM 2018.

On June 1 we discussed a paper by Dietsch et al that compares two approaches to checking program traces.

On May 25 we discussed the paper Property Checking Array Programs Using Loop Shrinking by Kumar et al from TACAS 2018.

 On May 18 we discussed the tutorial paper Automated Software Verification by Farzan et al.

Coding Session

 On May 11 we had a shared coding session. I.e., bring along your current coding project and let’s write some code...

Disambiguating Parser Conflicts

On May 4, Luís Eduardo de Souza Amorim from TU Delft gave a talk on his work to disambiguate conflicts in generalised parsers.


 Context-free grammars are widely used for language prototyping and implementation. They allow formalizing the syntax of domain-specific or general-purpose programming languages concisely and declaratively. However, the natural and concise way of writing a context-free grammar is often ambiguous. Therefore, grammar formalisms support extensions in the form of declarative disambiguation rules to specify operator precedence and associativity, solving ambiguities that are caused by the subset of the grammar that corresponds to expressions. Ambiguities with respect to operator precedence and associativity arise from combining the various operators of a language. While shallow conflicts can be resolved efficiently by one-level tree patterns, deep conflicts require more elaborate techniques, because they can occur arbitrarily nested in a tree. Current state-of-the-art approaches to solving deep priority conflicts come with a severe performance overhead. In this talk, I will present a novel low-overhead implementation technique for disambiguating deep associativity and priority conflicts in scannerless generalized parsers with lightweight data-dependency. By parsing a corpus of popular open-source repositories written in Java and OCaml, we found that our approach yields speedups of up to 1.73 x over a grammar rewriting technique when parsing programs with deep priority conflicts — with a modest overhead of 1 % to 2 % when parsing programs without deep conflicts.


On April 27 Tony Sloane gave a demo of the JupyterLab in-browser computational environment, including some discussion of support for non-notebook-traditional JVM-based languages such as Scala via the beakerx extension.

Analysis of JavaScript Programs

 On April 20 we will discussed a survey paper describing methods of analysis for JavaScript programs by Sun and Ryu. 

Author Obfuscation using Differential Privacy

 On April 6 Natasha Fernandes presented her MRes thesis work on A Novel Framework for Author Obfuscation using Generalised Differential Privacy.

Abstract: The problem of obfuscating the authorship of a text document has received little attention in the literature to date. Current approaches are ad-hoc and rely on assumptions about an adversary’s auxiliary knowledge which makes it difficult to reason about the privacy properties of these methods. Differential privacy is a well-known and robust privacy approach, but its reliance on the notion of adjacency between datasets has prevented its application to text document privacy to date. A relatively new approach to privacy known as generalised differential privacy extends differential privacy to arbitrary datasets endowed with a metric and permits the private release of individual data points. In this paper we show how to apply generalised differential privacy to author obfuscation, utilising existing tools and methods from the stylometry and natural language processing literature.

Learning Computing

On April 13 we discussed the following two papers:

On March 16 we discussed the following paper: Abstraction ability as an indicator of success for learning computing science? by Bennedssen and Caspersen.


 On March 9 we discussed two short papers about the applications and use of WebAssembly:

On March 2 we discussed the paper Mechanising and Verifying the WebAssembly Specification by Watt. More information on WebAssembly can be found at the project site.

On February 23 we discussed the paper Bringing the web up to speed with WebAssembly by Haas et al. More information on WebAssembly can be found at the project site.

Safety-Critical Use of a Formally-Verified Compiler 

On January 19 we discussed the paper CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler by Kästner et al.

Topics from 2017 

 Biography of a Process Model: The Formative Years

 On December 8 we hosted William M. Waite (Professor Emeritus, University of Colorado) who will present the following talk about the process he and colleagues have used to develop a general solution to the name analysis problem for programming languages. William has been active in programming languages and compiler construction research for more than fifty years, including co-authoring five books. He is a lead designer and developer of the Eli system for automation of compiler construction which is a joint project with Paderborn University and Macquarie University.

 Biography of a Process Model: The Formative Years

Process models are built to help us explain how the world works. A process model’s true beauty is in allowing us to predict process consequences, and thus to ultimately utilize the processes to achieve our own goals. Process models can be built for highly specialized circumstances, but become become more portable and valuable when crafted to address generalized situations. One common process in the world of computing finds the meaning of an identifier in a program. I’ll use this process to illustrate a typical coming-of-age path, from the initial development stages to the validation methods.

Predicate Abstraction

On December 1 we discussed the first part of the paper Constructing Quantified Invariants via Predicate Abstraction by Lahiri and Bryant.

The Contextual library for Scala

On November 24 we discussed the design and implementation of the Contextual library which 'is a small Scala library for defining your own string interpolators—prefixed string literals like url"" which determine how they are interpreted at compile-time, including any custom checks and compile errors that should be reported, while only writing very ordinary "user" code: no macros!'.

The Skink Program Verification Tool

 On November 10 Franck Cassez and Pongsak Suvanpong presented practice talks for the upcoming SAPLING workshop. Franck talked about the Skink verification tool being developed by himself, Tony Sloane, Matt Roberts and Pongsak in the Programming Languages and Verification group at Macquarie, focusing on the methods used by the tool and its capabilities. Pongsak presented preliminary results from his work to extend the verification method used by Skink to infer invariants for loops.  

Scala and SMT Solvers

On October 13 we discussed an upcoming Scala Symposium tool paper by Franck Cassez and Tony Sloane about an embedding of SMT solvers into Scala. Tony will give a practice version of the Scala symposium talk. We may also have a surprise talk...

 Hacking Session

 On September 15 we had a community hacking session.  Bring your laptop, your code and let's get some programming done...

Live Programming

On September 8 we discussed the paper "Towards Live Domain-Specific Languages: From Text Differencing to Adapting Models at Runtime” by van Rozen and van der Storm.

The Lean Theorem Prover

On August 4 we discussed Microsoft's Lean Theorem Prover via a short system description paper and tutorials on the Lean web site.

Language Server Protocol

On July 7 we discussed Microsoft's Language Server Protocol which is designed to sit between editors/IDEs and language servers that provide editor features such as completion, definition support etc. Details can be found in the project's github repository in particular in the documentation for Version 3.

Formalisation of Attribute Grammars

On June 30 Scott Buckley presented on his recent work to formalise parameterised, reference attribute grammars.

Software Engineering at Google

On June 23 we discussed the paper Software Engineering at Google by Fergus Henderson which details Google's key software engineering practices.


On June 2 we discussed the (draft) paper "The Final Pretty Printer" by Christiansen et al.


On May 26 we watched and discussed the talk "Clojure, Made Simple" by Rich Hickey from the JavaOne conference.

Type Systems as Macros

On May 19 we discussed the paper “Type systems as macros” by Chang et al that appeared at POPL 17.

Local Lexing

On May 5, we discussed the paper Local Lexing by Obua et al on a new way to make lexical analysis dependent on parsing without giving up separate lexers and parsers.

Attribute Grammar Semantics

On April 28, Scott Buckley presented an update on his work specifying the semantics of dynamically-scheduled attribute grammars.


On March 31 and April 7 we worked through parts of a tutorial about Verified Programming in F*. F* is a system that has a similar aim and approach to LiquidHaskell which we have reviewed in recent weeks but is part of the family of ML-based languages instead of working with Haskell.


On March 24 we continued discussing LiquidHaskell a system based on refinements of Haskell's types with logical predicates that lets you enforce critical properties at compile time. Our focus will be on some longer case studies from the LiquidHaskell tutorial book, particularly Chapter 5 on Refined Data Types and the following chapters on measures.

On March 17 we discussed a paper from Haskell 14 that gives an overview of LiquidHaskell a system based on refinements of Haskell's types with logical predicates that let you enforce critical properties at compile time.

Separation Logic

On February 24, March 3 and March 10, we discussed a tutorial by Peter O'Hearn on Separation Logic which is an extension of Hoare logic designed particularly for modelling heap structures.

Structural Operational Semantics

On February 17, we discussed Peter Mosses' paper Implicit Propagation in Structural Operational Semantics. This work builds on classical Structured Operational Semantics to define a way to extend semantic definitions to support new language features without having to retrofit new semantic information into rules that don't use it.

Topics from 2016  

Structural Operational Semantics

On December 9, we began discussing Gordon Plotkin's notes on Structural Operational Semantics. A series of separate meetings followed in December and January to cover most of the rest of the notes.

 Verifying Attribute Grammars

 On December 2, we discussed the paper "Formalising and Verifying Reference Attribute Grammars in Coq" by Schaefer et al from ESOP'09.

Hacking Session

On November 25, we had a group hacking session. Bring along your code to work on and discuss.

UPPAAL and Timed Automata

 On November 18, Peter Gjøl Jensen who is visiting us from Aalborg University in Denmark introduced us to UPPAAL, Timed Automata and how to solve the reachability problem using trace-abstraction-refinement. Interested attendees may want to check out a light-weight tutorial introduction to the tool and formalism or the UPPAAL tool website.

 Practice talks 

On October 21 Tony Sloane and Scott Buckley presented talks that are in preparation for the upcoming Scala symposium and a visit to Lund University. The titles and abstracts are:

  • The sbt-rats Parser Generator Plugin for Scala (Tony Sloane, Franck Cassez, Scott Buckley): Tools for creating parsers are a key part of a mature language eco-system. Scala has traditionally relied on combinator li- braries for defining parsers but being libraries they come with fundamental implementation limitations. An alternative is to use a Java-based parser generator such as ANTLR or Rats! but these tools are quite verbose and not ideal to use with Scala code. We describe our experiences with Scala- focused parser generation that is embodied in our sbt-rats plugin for the Scala Build Tool. At its simplest, sbt-rats pro- vides a bridge to the Rats! parser generator for Java. On top of this bridge, we have a simple grammar definition notation that incorporates annotations for tree construction and pretty-printing. As well as generating a Rats! grammar, sbt-rats can optionally generate case class definitions for the tree structure and a pretty-printer defined using our Kiama language processing library. We explain the sbt-rats gram- mar notation and describe our positive experiences using it to define grammars for LLVM assembly notation and the SMTLIB input/output language for SMT solvers.
  • CSS Layout with Attribute Grammars (Scott Buckley, Scala Symposium and Lund): CSS layout is a problem that is naturally described using attribute grammars. This talk demonstrates how Kiama’s attribute grammars are used to encode a more formal specification of the layout problem. In particular, we will examine how higher order reference attribute grammars can be used to create new ‘anonymous' structure in an existing tree, and how this can be made more transparent with Kiama’s attribute decorators. We will also touch on Scala’s extractor patterns and how they can change the way we phrase attribute grammar formulae.
  • Embedding Attribute Grammars (Tony Sloane, Lund): The Kiama library contains an embedding of dynamically scheduled attribute grammars in Scala. This talk will compare traditional approaches to attribute grammars with Kiama’s embedded approach. An aspect of particular focus will be the benefits and detriments of the embedding approach and of Scala in particular. Cooperation between Kiama’s attribute grammars and its term rewriting features will also be discussed.

 All Sorts of Permutations

 On October 14 we discussed the functional pearl "All Sorts of Permutations" by Christiansen et al from ICFP 2016.

The Boogie Verification Language

On October 7 we discussed the Boogie Verification Language via the paper "This is Boogie 2" by K. Rustan M. Leino.


On September 30 we finished discussing the paper Idris, a general-purpose dependently typed programming language: Design and implementation by Edwin Brady (skimming a lot of the detail).

On September 23 we continued discussing the paper Idris, a general-purpose dependently typed programming language: Design and implementation by Edwin Brady. We covered from 2.5 to 3.3 (inclusive).

On September 16 we began discussing the paper Idris, a general-purpose dependently typed programming language: Design and implementation by Edwin Brady.


On September 9 we looked at an introduction to the functional programming language PureScript. Attendees who wish to try out examples should install PureScript using these instructions

Dependent Types

On August 19 and September 2 we discussed the paper "An Abstract Memory Functor for Verified C Static Analysers" that will appear at ICFP 2016. 

On August 12 we discussed a paper from ESOP 2007 on dependent types for low-level programming.

Silver attribute grammar system 

On August 5 we discussed an overview paper on the Silver attribute grammar system

ECOOP LIVE Workshop 2016

On July 22 we looked at papers and demos from the recent ECOOP LIVE Workshop 2016

Dynamic Witnesses for Static Type Errors

On July 8 we discussed the paper "Dynamic Witnesses for Static Type Errors" by Seidel et al which looks at how to explain type errors using counterexamples. 

The Leon Verification System

 On July 1 we discussed the paper "Satisfiability modulo recursive programs" Suter et al which provides more detail on how the Leon Scala-based verification system works.

On June 24 we discussed the paper "An overview of the Leon verification system: verification by translation to recursive functions" by Blanc et al from Scala '13.

The Racket Programming Language

On June 17 we watched and discussed the talk Racket: A Programming-Language Programming Language by Robby Findler from YOW LambdaJam 2015.

Software Verification 

On June 10 we discussed the paper Summary-Based Inter-Procedural Analysis via Modular Trace Refinement by Cassez et al.

On June 3 we discussed the paper Inferring Loop Invariants Using Postconditions by Furia and Meyer.

On May 20 we discussed the paper "Witness Validation and Stepwise Testification across Software Verifiers" by Beyer et al.

On May 13 we discussed the paper "Loop Invariants on Demand" by Leino and Logozzo.

 On April 8 and May 6 we discussed the paper "Predicate abstraction for software verification" by Flanagan and Qadeer from POPL 2002.

Dependent Object Types

On March 18 we will discuss The Essence of Dependent Object Types by Amin et al which describes recent work on new type theory for the Dotty project which may become the successor of Scala (or a later Scala version).

Workflow systems

On February 26 we discussed the paper "A Semantic Framework for Automatic Generation of Computational Workflows Using Distributed Data and Component Catalogs" by Yolanda Gil et al. This is long paper so we will focus mostly on the problem space, motivation and a high-level view of the system.


On February 19 we discussed the paper "Galaxy: a comprehensive approach for supporting accessible, reproducible, and transparent computational research in the life sciences" by Jeremy Goecks , Anton Nekrutenko, James Taylor, and The Galaxy Team. This is a background paper for future weeks where we will most likely continue on this topic in the area of workflow systems and domain-specific languages aimed at this problem area.


On February 12 we discussed the paper "Programming and Reasoning with Algebraic Effects and Dependent Types" by Edwin Brady from ICFP'13.
On February 5 we discussed the paper "Freer Monads, More Extensible Effects" by Oleg Kiselyov and Hiromi Ishii from Haskell'15.


Role-Based Programming

On January 29, our visiting student Max Leuthäuser talked about his work.

Beyond Roles at Runtime

Max Leuthäuser

TU Dresden

Current role-based programming languages do not support customisable role dispatch. Such a highly dynamic mechanism is required to resolve invocation ambiguities appearing with the rich semantics of role-playing objects. This talk will introduce a Scala-based solution in depth. Later, transferring the implementation pattern behind it to programming with reference-attribute grammars is one important step towards safe and adaptive software, e.g. in the context of cyber-physical systems.

Topics from 2015

Computational Category Theory

In July we are studying the computational category theory notes.  You won't need to know ML to follow along, we are Haskell and Scala people after all.

  •  July 24: Categories and Functors (skim the earlier chapters)
  • July 31: Limits and Co-limits

Monto Disintegrated Development Environment

On July 10 we discussed the Monto Disintegrated Development Environment that is being developed at Macquarie. The aim of Monto is to provide features similar to those of integrated development environments such as Eclipse, but require much less effort on the part of developers to provide new components for the environment. We'll look at the architecture and implementation of as well as demonstrate some features that have been implemented so far.

 Hacking Session 

On June 26 we held a hacking session: Bring along your parsers, pretty-printers, code generators, compilers, etc for a joint coding session. In particular, if you want to use the Kiama library and/or sbt-rats parser generator we've talked about in recent weeks, now's the time to try.

sbt-rats Parser Generator

On June 19 we discussed the sbt-rats parser generator that has been developed here at Macquarie. sbt-rats provides an sbt plugin that enables the Rats! parser generator to be used in Scala projects. The parser can be specified directly using a Rats! specification or using a simplified syntactic notation. The syntactic notation can also be translated into a Scala implementation of abstract syntax trees and a pretty printer for those trees. Pretty-printing support is provided by the Kiama language processing library.


 On June 12 we discussed the Strategic Term Rewriting portion of the Kiama language processing library.

 On June 5, we discussed the attribute grammar part of the Kiama language processing library based on a paper from Science of Computer Programming

 On May 22 Tony Sloane gave an overview of the Kiama language processing library that has been built at Macquarie. The overview included a simple, complete example of using Kiama to build a simple software language processor.

Trace Abstraction

On May 15 we will discuss the paper Refinement of Trace Abstraction by Heizmann et al.

Program Slicing

On May 8 we continued discussing program slicing and the paper "A Survey of Program Slicing Techniques" by Frank Tip, focusing on Section 3.2 onwards.

On April 24 we continued our discussion of program slicing by looking at the first three sections of the paper "A Survey of Program Slicing Techniques" by Frank Tip.

On April 17 we discussed the classic paper "Program Slicing" by Mark Weiser. Slicing is a program transformation technique that in its simplest form seeks to remove code from a program that cannot affect the value of a  variable at a particular point. It is useful for debugging and program analysis tasks where we want to restrict the focus of attention to the subset of code that might be affecting some result, rather than have to consider the whole program.

LLVM in Scala

On April 10 Tony Sloane described progress on the library he is building to allow LLVM code to be processed in Scala. At present the library provides a parser, tree constructor and pretty-printer for LLVM intermediate representations. Discussion will centre around the suitability of this tree representation for further processing or generation from Scala, particularly on the design of  a higher-level representation to make processing and generation easier.

Attendees who are unfamiliar with LLVM may find it useful to read "LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation" which provides an overview of the aims and approaches of the LLVM project.

Programming Language Design

Domain-Specific Profiling

On March 13, we discussed some work that Tony and Matt have done over the last couple of years on general profiling approaches for domain-specific languages.

Strategic Programming Errors

On March 6, we discussed work that Matthew Roberts has begun on characterising errors that arise when using strategic programming. A start on some typical examples can be found at this page.

Abstract State Machines

On February 27, we discussed the use of Abstract State Machines to specify the semantics of the Java programming language and the Java Virtual Machine. Tony Sloane presented a walk-through of simple versions of these machines to give an idea of how the method works.

On February 13, we continued our discussion of Abstract State Machines by looking how they are provided by the Kiama language processing library developed here at Macquarie. Matt Roberts showed how they can be used to model psychological processes. Tony Sloane gave a short walk-through of  the Kiama implementation of ASM.
On February 6 we started discussing Abstract State Machines which are a generalisation of finite-state machines for system specification. Our source was a primer on ASMs by Huggins and Wallace.

Topics from 2014

How to Design Programs
On October 17 to November 28 we discussed  "How to Design Programs" by Felleisen et. al. 

Flow Fusion
On October 3 we hosted a guest speaker Ben Lippmeier talking about his work on applying flow fusion in compilers to scale computations to large data sets.

Flow Fusion for the Biggest Data
Ben Lippmeier 

The great MapReduce has fallen and shattered into myriad creatures: Pig, Impala, Dryad, Naiad, Dremel, Druid, and Shark to name a few. Once revered as the gateway to the biggest data, raw MapReduce is now being covered up and pushed aside in favour of faster and easier approaches. The myriad creatures Pig, Impala, Dryad and so on are languages and systems for distributed programming, largely originating from the databases community. Although they seem like a disparate collection at first, on closer inspection they turn out to share a common data-parallel data-flow architecture. Not mere databases, most are general purpose programming environments which support computational workloads consisting of arbitrary user defined-code. Not mere programming environments, some embed full language runtimes and compile incoming queries to native code on the fly. Though this lens the modern distributed database is a full language, compiler, and runtime -- query optimisation is data-flow program optimisation, and query compilation is data-flow program compilation. The functional programmers in the audience will know that data-flow programs are also first-order functional programs, so they're that too.

In this talk I'll give an overview of the myriad creatures, then present my recent work on query / data-flow compilation. Existing compilation methods cannot fuse general branching data-flows -- meaning that if a produced table is consumed by several physical operators it may be materialised in memory (or on disk) in an intermediate stage. Flow fusion is an approach to compile such data-flows into single imperative loops that do not require intermediates to be materialised. I'll also talk about the ramifications for query planning -- choosing to fuse clusters of operators into single loops prevents others from being fused. In recent joint work we reduce this query planning problem to an Integer Linear Programming problem and use an external solver to compute the optimal clustering.

Respect Your Parents: How Attribution and Rewriting Can Get Along

On August 29 Tony Sloane gave a practice version of an upcoming SLE 2014 talk.

Attribute grammars describe how to decorate static trees. Rewriting systems describe how to transform trees into new trees. Attribution is undermined by rewriting because a node may appear in both the source and product of a transformation. If an attribute of that node depends on the node’s context, then a previously computed value may not be valid. We explore this problem and formalise it as a question of ancestry: the context of a node is given by the tree’s parent relationships and we must use the appropriate parents to calculate attributes that depend on the context. We show how respecting parents naturally leads to a view of context-dependent attributes as tree-indexed attribute families. Viewed in this way, attribution co-exists easily with rewriting transformations. We demonstrate the practicality of our approach by describing our implementation in the Kiama language processing library

Joint work with Matt Roberts and Len Hamey.

Type Inference for the Spine View of Data

On August 22 Matt Roberts gave a practice version of his upcoming WGP 2014 talk.

In this work we describe both a type checking and a type inference algorithm for generic programming using the "spine view" of data. The spine view of data is an approach to decomposing data in functional programming languages that supports generic programming in the style of Scrap Your Boilerplate and Stratego. The spine view of data has previously been described as a library in a statically typed language (as in Haskell), as a language feature in a dynamically typed language (as in Stratego), and as a calculus of patterns (as in the Pattern Calculus). The contribution of this paper is a type inference algorithm for the spine view and a sound type relation that underlies this inference algorithm. The type inference algorithm does not require any type annotations to be added in support of the spine view. This type inference algorithm is an extension of Hindley-Milner type inference, thus showing how to introduce the spine view of data as a language feature in any functional programming language based on Hindley-Milner.

Joint work with Tony Sloane.

Visual Dataflow Languages, Attribute Grammars

On August 15 we hosted a visitor Niklas Fors who is a PhD student at Lund University in Sweden. He will give a short presentation on his work building extensible  visual dataflow-based languages (abstract below). We will also discuss attribute grammar systems, since Niklas' supervisor Prof Görel Hedin and colleagues are responsible for a number of contributions in that area, most notably reference attribute grammars and the JastAdd system.

Intercepting Dataflow Connections in Diagrams with Inheritance 

Niklas Fors and Görel Hedin

Control systems are often built using visual dataflow-based languages, and supporting different variants may be challenging. We introduce the concept of connection intercep- tion based on inheritance. This mechanism allows a diagram to extend another diagram and intercept connections defined in the supertype, that is, to replace it by two other connections, in order to specialize the behavior. This can be used to create extensible libraries that support different variants.


On August 1, James Moss gave a demo of his undergraduate winter project work on embedding a DSL in  Swift.

Language Workbenches

On July 11 we discussed a recent paper on the start of the art in language workbenches.

Type and Effect Systems

On June 27th we discussed a paper on Type and Effect Systems by Flemming Nielson and Hanne Riis Nielson.


On June 20th we watched and discussed a recent talk by Martin Odersky on "Scala: The Simple Parts".


On June 6th we investigated Apple’s new programming language Swift via some readings and a demo.

Language-Oriented Programming

On May 16 and 23 we discussed Language-Oriented Programming, based on two overview articles: Language-Oriented Programming: The Next Paradigm and  From Programming To Modeling – and back again. This week provides background for future discussions of JetBrains' MPS development environment.


On May 2 we discussed an unpublished paper about the language Katahdin: Mutating a Programming Language’s Syntax and Semantics at Runtime.


On April 4 we conducted a partial  tour through the Ceylon language from Red Hat. Only the first few sections were covered.


On March 28 we will discuss a paper about Parallaxis-III a language for architecture-independent data parallel processing.

Data Parallel Haskell

On March 21 we will discuss a status report from the Data Parallel Haskell project which aims to achieve expressive, efficient nested data parallel computation in the Haskell language.

Maxine Java VM

On March 14 we discussed a paper about the Maxine Java VM that is written in Java and is intended to form a more practical basis for teaching and research than the mainstream JVM implementations.

F# Active Patterns

On Feb 28 we discussed F#'s facilities for extensible pattern matching by reading an ICFP 2007 paper on the topic.

F# Type Providers

On Feb 21 we discussed F#'s Strongly-Typed Language Support for Internet-Scale Information Sources (i.e., type providers).


In the first meeting for 2014 on Feb 14 we eased into the world of programming languages again by watching a couple of tutorial videos (one and two) on the .NET-based functional language F#.

Topics from 2013


On December 6 we discussed a paper from Onward! 2012 about the social aspects of programming language adoption.

Formal modelling of semantics

On November 29 we discussed introductory tutorials for the Racket language and the Redex semantic modelling DSL.

On November 22 we discussed a paper from POPL 2012 about mechanisation of semantic models in the Racket language.

Path Expressions

On November 15 we will discuss two early papers about using path expressions to coordinate concurrent processes:

Language Support for Component Lifecycles

On November 1 and 8 Kym Haines presented some of his language design ideas. This is early stages of a work in progress about developing language features that support:

  • integrating program components based on a component's usage lifecycle
  • enforcing correct usage of program components through their usage lifecycle

Includes a demo and description of:

  • a language with static typing where types are optional and functions do not have explicit argument declarations
  • a mechanism for enforcing correct usage of program components through their usage lifecycle

Applications of Dependent Types

On October 25 we discussed the use of dependent types to express properties of grammars and grammar transformations in a paper by Brink et al.

Border handling in an image processing domain-specific language

On October 4 and 18 we discussed a draft paper that reports work from Len Hamey's recent Outside Studies Program. Len is looking for feedback to help improve the paper. If you plan on attending, please email Tony for a copy of the paper and he will email it to you.

Calculus of (Inductive) Constructions

On September 27 we continued our discussion of the Calculus of Inductive Constructions by reading Section 4.5 of the Coq reference manual.

On September 20 we continued our discussion of the Calculus of Constructions and related calculi by starting the Calculus of Inductive Constructions chapter of the Coq reference manual.

On September 13 we began discussing the paper by Coquand and Huet that formalised the Calculus of Constructions a formalism that sits beneath proof systems such as Coq.

Rust Programming Language

On August 30, we continued discussed the Rust Programming Language from Mozilla Research particularly the  Rust Language Tutorial sections 7-12 and the supplementary tutorials on Borrowed Pointers and Macros.

On August 23, we discussed the Rust Programming Language from Mozilla Research by looking at the Rust Language Tutorial.

Live Programming

On August 16, we continued our discussion of live programming environments by looking at Light Table a project under development by Chris Granger and colleagues. We will look at some demos and try the alpha release.

On August 9, we continued discussing presentations from the Live 2013 workshop, at least the papers Introducing Circa: A dataflow-based Language for Live Coding,  Interactive Code Execution Profiling, and  Making Methods Live in Newspeak.

On August 2, we discussed two papers about Live Programming: one by Steven Tanimoto who tries to put modern live programming into an historical perspective [1], and one by Sean McDermid on live programming research at Microsoft [2]. We also watched a couple of the demonstration videos from the Live 2013 workshop: Improvisation on a live-coded mobile musical instrument using urMus and  Visual code annotations for cyberphysical programming.

Functional Programming Type Systems

On June 21 and 28 we looked at Daan Leijen's system for type inference in the presence of higher-order polymorphism

On June 7 we looked at Mark Jones's system for type inference in the presence of higher-order polymorphism.

DSLs for image processing and low-level computer vision

On May 24 Len Hamey gave us an update on his current work to extend the Halide image processing library.


On May 10, Tony Sloane and Matt Roberts discussed the Kiama language processing library that we have built here at Macquarie. This session was a practice for our talk and workshop at the YOW! LambdaJam conference in Brisbane the following week.


On April 19, 26 and May 3, we discussed Edwin Brady's dependently-typed programming language Idris by working through the Idris tutorial.

Syntax Definition

On April 12, we discussed the SPLASH Onward! 2010 paper  Pure and declarative syntax definition: paradise lost and regained by Kats and Visser.

Origin Tracking

On April 5, we discussed the original paper on origin tracking in rewriting systems by van Deursen, Klint and Tip. Origin tracking traces the source positions of terms from input to output as rewrites happen, thereby enabling messages associated with rewritten terms to be reported with respect to the original source.


On March 22, we discussed Oleg Kiselyov's paper on Iteratee IO which is attracting quite a bit of attention for developing communication streams with precise resource control.

Hack Your Language! course

On March 15, we discussed Ras Bodik's "Hack Your Language!" undergraduate course on programming languages that he teaches at Berkeley. In particular, we will discuss the motivation for the course as set out in an overview from 2011 and a 2008 paper. We also looked at the materials for the course that are available on its web site.

DSLs for image processing and low-level computer vision

Early DSL's in this area used procedural programming style and focused on automatic parallelisation of kernel processing. Apply and Brook are examples. Another approach developed late last century is parallel procedural programming with arrays as first-class objects exemplified by ZPL. In contrast, halide, developed recently at MIT, is a functional programming DSL for image processing. Embedded in C++, user code is JIT compiled at runtime or can be precompiled. Halide programs are at least as efficient as hand tuned algorithms. Backends target Intel architecture, ARM and CUDA with parallelisation and SSE vectorization.

On February 22 after a brief introduction from Len, we discussed a paper about the halide language.

On March 1 we continued our discussion from February 22, particularly looking at the implementation techniques used by the Halide DSL and Len presented some of his thoughts for useful extensions and improvements.

On March 8 we continued our discussion from March 1, particularly discussing how the Halide image processing language uses the LLVM framework.

Optimizing Data Structures

On February 15 we discussed part of the paper "Optimizing Data Structures in High-Level Programs: New Directions for Extensible Compilers based on Staging", by Rompf et al from POPL 2013. This paper discusses how to staged computation to define internal compiler passes which can yield order of magnitude speedups.

String Interpolation in Scala

On February 8 Tony Sloane talked about the new string interpolation features of Scala 2.10, leading to a discussion of implementing concrete object syntax using string interpolation and macros (also new in Scala 2.10).

Inventing on Principle

On February 1 we watched and discussed a video of Bret Victor's talk Inventing on Principle. This talk received a great deal of attention in 2012 and is a major inspiration for the current live programming movement .

Topics from 2012

Scrap Your Boilerplate

On December 14 we discussed the first paper in the "Scrap Your Boilerplate" series which shows how to do generic programming in Haskell using an approach based on typed strategic programming:
Scrap your boilerplate: a practical approach to generic programming by Ralf Laemmel and Simon Peyton Jones.

Types for Strategies

On November 30 we discussed the application of the ideas from Laemmel's Typed generic traversal with rewrite strategies paper to the Kiama library's rewriting component.

On November 16, we continued our discussion of type systems for generic rewrite strategies based on the paper "Typed generic traversal with term rewriting strategies" by Ralf Laemmel. This week we focused on section 4.

On November 9, we continued our discussion of type systems for generic rewrite strategies based on the paper "Typed generic traversal with term rewriting strategies" by Ralf Laemmel. This week we focused on section 2.4 and the beginning of section 3 up to the type rules of Figure 10.

On November 2, we began a discussion of type systems for generic rewrite strategies. Our discussion will be based on the paper "Typed generic traversal with term rewriting strategies" by Ralf Laemmel. This week we focused on the background and motivation from sections 1 and 2.


On October 26, we discussed the new TypeScript language from Microsoft. To guide the discussion we will watch the video "Introducing TypeScript" by Anders Hejlsberg. More information on TypeScript, including the language specification, is available from the main TypeScript site.

Software Failure Diagnosis with Spectral Debugging

In the second hour on October 19, we hosted an external speaker, Jason Lee speaking on software failure diagnosis.

Abstract: In my research area, I am investigating approaches to assist diagnosis of failures in software program. Program statements or blocks are ranked according to how likely they are to be buggy, based on what statements are executed in test cases. A very simple single-bug program is used to model the problem. By examining different possible execution paths through this model program over a number of test cases, the effectiveness of different proposed spectral ranking methods can be evaluated in idealized conditions. The results are remarkably consistent to those arrived at empirically using the Siemens test suite and Space benchmarks. I also investigated different approaches on multiple-bug programs by using different weights for failed tests to provide information to the bug. Finally, I looked into using frequency information of test coverage to help locate bugs more effectively as compared to using binary information. These approaches showed improved significant bug localization performance across the above mentioned benchmarks.

Biography: Lee Hua Jie received his Bachelor of Information Technology (HONS.) majoring in Software Engineering from the Multimedia University, in 2005. He started working in the software industry as a Software Engineer and Software Validation Engineer with Motorola Technology and iWOW Pty. Ltd. respectively. In 2007, he was offered the International Postgraduate Research Scholarship (IPRS) from DEEWR to do his PhD in the Department of Computer Science and Software Engineering, the University of Melbourne. His research interests include spectral debugging, which uses test coverage information to help programmers locate bugs effectively. He has been working with DOLBY LABS AUSTRALIA since July 2011 as a Senior Software Test Engineer. He is still actively pursuing research in his free time and contributes to the research field as technical reviewer for international conferences (IWESEP 2010, IWESEP 2011, COMPSAC 2012, APSEC 2012) and Advances in Software Engineering journal.

Object Algebras

On October 19, in the first hour we continued our discussion of object algebras from last week, looking at a Scala implementation and considering alternative implementations as raised in our discussion from last week.

On October 12, we discussed a paper on solving the expression problem using object algebras by Bruno Oliveira and William Cook. This paper won the best paper award at ECOOP 2012.

Turing-Complete Templates

On September 28, we discussed an article on Turing-Complete Templates in liftweb by Matt Roberts.

Parsing with Derivatives

On September 21, we discussed an ICFP 2011 paper on Parsing with Derivatives by Might, Darais and Spiewak.

Controlled Natural Languages

On September 14, Rolf Schwitter from Macquarie University presented some of his work on controlled natural languages:

Answer Set Programming via Controlled Natural Language Processing

Controlled natural languages are subsets of natural languages that can
be used to describe a problem in a very precise way, furthermore they
can often be translated automatically into a formal notation. We
investigate in this paper how a controlled natural language can be
used as a specification language for Answer Set Programming (ASP). ASP
is a declarative approach to problem solving and has its roots in
knowledge representation, logic programming, and constraint
satisfaction. Solutions of ASP programs are stable models (= answer
sets) that build the starting point for question answering. As a proof
of concept, we translate a problem specification written in controlled
natural language into an ASP program and compute a stable model that
contains the answers to a number of questions.


On September 7, we discussed a paper about the history of the Lua programming language. Lua began as a simple configuration language but has expanded to a general scripting language to rival more well-known counterparts such as Python and Ruby. Lua is particularly widely used as a scripting language for game platforms.

Concrete object syntax

On August 31, we continued our discussion of concrete object syntax as realised by the SDF and Stratego program transformation tools. Two papers were discussed: a paper on SDF support for concrete syntax and a paper on an application of these ideas to concrete syntax for a Prolog-based program synthesis system.

On August 24, we discussed the paper "Concrete syntax for objects" by Martin Bravenboer and Eelco Visser (OOPSLA 2004). This work presents a solution to the problem of embedding the syntax of a language within another language.

sbt-rats: packrat parser generation for Scala

On August 17, Tony Sloane gave a talk about his sbt-rats plugin for the Scala simple build tool, which provides support for using the Rats! parser generator from Scala.

Topics from 2011

Components in Scala

On December 2 and 16 we discussed the paper Scalable Component Abstractions by Odersky and Zenger.


On November 11, we examined monadic code as a Scala state monad used in a simple partial evaluator.

On November 4, we continued discussing monads as a program structuring mechanism using the comprehensive introduction Monads for functional programming by Philip Wadler.

On October 28, we discussed monads as a program structuring mechanism using the comprehensive introduction Monads for functional programming by Philip Wadler.


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.


On October 14, we discussed the CoffeeScript language, based on the language documentation.


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. Demos will also be given in this talk.


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:

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.

  • 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
  • August 5:
    • the remainder of the Basics chapter, and
    • the Lists: Products, Lists and Options chapter
  • August 12:
    • the Poly: Polymorphism and Higher-Order Functions chapter
  • 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.

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.

System Software Verification

On June 10 we discussed the paper Bringing Extensibility to Verified Compilers by Tatlock and Lerner from PLDI 2010.


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 subtyping 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.


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.


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 measureable benefits
compared to applications written in general-purpose languages.

His research interests include programming languages, software
engineering and operating systems.

(For more information, see

Version control theory

On Feb 11, we discusseded a paper 1 that presents a formalisation of the patch theory of the Darcs revision control system.


Topics from 2010


On December 17 we looked at the [Clang C/C++/Objective-C front-end": for the LLVM compiler infrastructure. In particular, we will watch the State of Clang video from the 2009 LLVM Developer's Meeting.

On December 10 we looked at the Haskell bindings for the LLVM compiler infrastructure. As a starting point, we will look at the following blog posts:

On November 26, Tim Morton presented his COMP188 project "LLVM IR Tree Encoding in Scala".


LLVM as a compiler framework presents a wide number of attractive tools for language developers, such as code generation support for a wide number of target platforms, and a modern source/target independent optimizer, all built around a well specified intermediate code representation. Furthermore, the LLVM core libraries are well- documented. The LLVM core libraries are written in C+, however, and Scala also presents other attractive features for compiler development, such as functional language features and excellent support for pattern matching, in contrast to C+. It would be advantageous if we could devise a way to best utilise LLVM/Scala¿s respective features, and obtain ¿the best of both worlds¿ for language developers.

The aim of this work is to investigate doing exactly that, to construct a library where front-end compilation can be carried out in Scala, and back-end compilation is completed in LLVM, with minimal effort - by taking advantage of the fact that the LLVM compiler framework is built around the LLVM intermediate representation.

Parsing and unparsing combinators

On October 29 and November 5, we discussed a paper 1 that describes a new method for constructing parser combinators that guarantee termination while still allowing many forms of left recursion.

1 Danielsson, N. A. Total parser combinators. In ICFP ¿10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (New York, NY, USA, 2010), ACM, pp. 285¿296.

On October 22, we discussed a paper 1 that describes "Syntactic Descriptions", a method for combining the parsing and unparsing aspects of a language description.

1 Rendel, T., and Ostermann, K. Invertible syntax descriptions: unifying parsing and pretty printing. In Haskell ¿10: Proceedings of the third ACM Haskell symposium on Haskell (New York, NY, USA, 2010), ACM, pp. 1¿12.

Effect Systems

On October 1, we discussed a paper 1 that describes a generic system for statically reasoning about effects in programs.

1 Marino, D., and Millstein, T. A generic type-and-effect system. In TLDI ¿09: Proceedings of the 4th international workshop on Types in language design and implementation (New York, NY, USA, 2009), ACM, pp. 39¿50.

Applied Type System (ATS)

On September 24, we discussed a paper 1 that describes the Applied Type System method for combining programming with theorem proving.

1 Chen, C., and Xi, H. Combining programming with theorem proving. In Proceedings of the International Conference on Functional Programming (New York, NY, USA, 2005), vol. 40(9) of SIGPLAN Notices, ACM, pp. 66¿77.

Polymorphic Type inference

On September 17, we discussed a paper 1 that presents a another method for type inference in polymorphic functional languages.

1 O¿Toole, Jr., J. W., and Gifford, D. K. Type reconstruction with first-class polymorphic values. In PLDI ¿89: Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation (New York, NY, USA, 1989), ACM, pp. 207¿217.

On September 10, we discussed a paper 1 that presents a method for type inference in polymorphic functional languages.

1 Leijen, D. HMF: simple type inference for first-class polymorphism. In Proceedings of the International Conference on Functional Programming (New York, NY, USA, 2008), vol. 43(9) of SIGPLAN Notices, ACM, pp. 283¿294.

August 27, September 3: Lazy Evaluation

On September 3, we discussed a a paper 1 that builds on last week's paper to derive an abstract machine implementation of lazy evaluation.

1 Sestoft, P. Deriving a lazy abstract machine. Journal of Functional Programming 7, 03 (1997), 231¿264.

On August 27, we discussed a paper 1 on semantics of lazy evaluation in functional languages.

1 Launchbury, J. A natural semantics for lazy evaluation. In POPL ¿93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (New York, NY, USA, 1993), ACM, pp. 144¿154.

August 20: System Modelling and Design using Event-B

On August 20, Ken Robinson from UNSW talked about system modelling and design using Event-B and the Rodin tool. Ken has kindly agreed to let members of the group read a draft of his upcoming book on this topic 1. Chapters 2 and 3 give a basic introduction, with Chapters 4 and 5 providing more depth.

1 Ken Robinson, System Modelling & Design using Event-B, draft manuscript.

July 30, August 6: Verified Programming Language Processing

On August 6 we discussed a paper 1 that describes the Ott tool and the support that it provides for programming language semantics researchers.

1 Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., and Strnisa, R. Ott: Effective tool support for the working semanticist. Journal of Functional Programming 20, 1 (2010), 71¿122.

On July 30 we discussed a paper 1 that describes how referenced attribute grammars have been verified using the Coq proof assistant.

1 Scha ?fer, M., Ekman, T., and de Moor, O. Formalising and verifying reference attribute grammars in Coq. Programming Languages and Systems (2009), 143¿159.

May 28, June 11, 18, 25: Compiler Correctness

On June 25 we discussed a paper 1 that describes how programs can be extracted automatically from proofs of correctness using the Coq proof assistant.

1 Letouzey, P. Extraction in Coq: An overview. In Logic and Theory of Algorithms (2008), no. 5028 in Lecture Notes in Computer Science, pp. 359¿369.

On June 18 we continued discussing the CompCert project by walking through some of the formal specification of the Clight to Cminor translation and correctness proof 1.


On June 11 we continued discussing the CompCert project by considering a paper 1 on verification of the compiler front-end.

1 Blazy, S., Dargaye, Z., and Leroy, X. Formal verification of a C compiler front-end. In FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings (2006), J. Misra, T. Nipkow, and E. Sekerinski, Eds., vol. 4085 of Lecture Notes in Computer Science, Springer, pp. 460¿475.

On May 28 we discussed a paper by Xavier Leroy on formal verification of compilers 1.

1 Leroy, X. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107¿115.

May 21: Running the NIM Next-Generation Weather Model on GPUs

On May 21 we hosted the following talk:

Running the NIM Next-Generation Weather Model on GPUs

Mark Govett
NOAA, Boulder, Colorado

We are using Graphical Processor Units (GPU)s to run a new weather model, called the Non-hydrostatic Icosahedral Model (NIM), being developed at NOAA¿s Earth System Research Laboratory (ESRL). The parallelization approach is to run the entire model on the GPU and only rely on the CPU for model initialization, I/O, and inter-processor communications. We have written a compiler, using the Eli Compiler Construction Tool, to convert Fortran into CUDA, and used it to parallelize the dynamics portion of the model. Dynamics, the most computationally intensive part of the model, is currently running 34 times faster on a single GPU than the CPU. This presentation will briefly describe the NIM model, our compiler development, and parallelization results to date. I will also describe recent work evaluating commercial Fortran GPU compilers, and progress to date running the NIM on multiple GPUs.

March 19, 26, April 9, May 7, 14: Scala

On May 14 we watched a short video talk 1 and discussed a paper 2 that explain how type specialization has been added to the Scala implementation.

1 Scala Days 2010 talk: Type Specialization in Scala by Iulian Dragos

2 Dragos, I., and Odersky, M. Compiling generics through user-directed type specialization. In ICOOOLPS ¿09: Proceedings of the 4th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems (New York, NY, USA, 2009), ACM, pp. 42¿47.

On May 7 we watched a short video talk 1 and discuss a paper 2 that describe how named and default arguments were added to the Scala language.

1 Scala Days 2010 talk: Named and Default Arguments in Scala by Lukas Rytz

2 Rytz, L., and Odersky, M. Named and default arguments for polymorphic object-oriented languages: a discussion on the design implemented in the Scala language. In SAC ¿10: Proceedings of the 2010 ACM Symposium on Applied Computing (New York, NY, USA, 2010), ACM, pp. 2090¿2095.

On April 9 we discussed a paper 1 that compares facilities for generic programming in Scala with those in Haskell.

1 Oliveira, B. C., and Gibbons, J. Scala for generic programmers. In WGP ¿08: Proceedings of the ACM SIGPLAN workshop on Generic programming (New York, NY, USA, 2008), ACM, pp. 25¿36.

On March 26 we discussed a paper 1 on the compilation of Scala structural types for the Java virtual machine.

1 Dubochet, G., and Odersky, M. Compiling structural types on the JVM: a comparison of reflective and generative techniques from Scala¿s perspective. In ICOOOLPS ¿09: Proceedings of the 4th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems (New York, NY, USA, 2009), ACM, pp. 34¿41.

On March 19 we discussed a paper 1 on the design of the Scala 2.8 collection library.

1 Fighting bit rot with types (Experience Report: Scala Collections), Martin Odersky and Adriaan Moors, Leibniz International Proceedings in Informatics, 2009.

March 2: Control Flow Analysis

On Tuesday March 2, 4-6pm, E6A357, we hosted the following visitor talk.

Harry Mairson, Brandeis University, Linear Logic and the Complexity of Control Flow Analysis

Static program analysis is about predicting the future: it's what compilers do at compile-time to predict and optimize what happens at run-time. What is the tradeoff between the efficiency and the precision of the computed prediction? Control flow analysis (CFA) is a canonical form of program analysis that answers questions like "can call site X ever call procedure P?" or "can procedure P ever be called with argument A?" Such questions can be answered exactly by Girard's geometry of interaction (GoI), but in the interest of efficiency and time-bounded computation, control flow analysis computes a crude approximation to GoI, possibly including false positives.

Different versions of CFA are parameterized by their sensitivity to calling contexts, as represented by a contour¿a sequence of k labels representing these contexts, analogous to Lévy's labelled lambda calculus. CFA with larger contours is designed to make the approximation more precise. A naive calculation shows that 0CFA (i.e., with k=0) can be solved in polynomial time, and kCFA (k>0, a constant) can be solved in exponential time. We show that these bounds are exact: the decision problem for 0CFA is PTIME-hard, and for kCFA is EXPTIME-hard. Each proof depends on fundamental insights about the linearity of programs. In both the linear and nonlinear case, contrasting simulations of the linear logic exponential are used in the analysis. The key idea is to take the approximation mechanism inherent in CFA, and exploit its crudeness to do
real computation.

This is joint work with David Van Horn (Northeastern University).

February 26 and March 12: Agda

On February 26 we started discussing a tutorial 1 on Agda, which is a dependently typed functional programming language and proof assistant.

1 Dependently typed programming in Agda, Ulf Norell, Advanced Functional Programming Summer School, 2008

February 12 and 19: Language Embedding

On February 19 we discussed "Domain specific language implementation via compile-time meta-programming" by Tratt 1 which describes a method for implementing domain-specific languages by embedding them into another language.

1 Tratt, L. Domain specific language implementation via compile-time meta-programming. ACM Trans. Program. Lang. Syst. 30, 6 (2008), 1¿40.

On February 12 we discussed "Formalizing Homogeneous Language Embeddings" by Clark and Tratt 1 which describes a method for ensuring safety when multiple domain-specific languages are embedded in a host language.

1 Clark, T., and Tratt, L. Formalizing Homogeneous Language Embeddings. In Preliminary Proceedings of the Ninth Workshop on Language Descriptions Tools and Applications LDTA 2009 (2009).

Topics from 2009

December 4: Program Obfuscation

On December 4 we discussed a paper 1 and accompanying web page 2 on the issue of whether program obfuscation is possible. This was the final meeting for 2009.

1 On the (Im)possibility of Obfuscating Programs, Barak, et. al., Crypto 2001,

November 27: Google's Go language

On November 27 we watched an overview talk 1 about Google's new Go programming language.

1 Rob Pike, The Go Programming Language, Google Tech Talk, October 30, 2009.

October 9, 23: Clojure

On October 9 and 23 we watched a talk by Rich Hickey about his Clojure language, which is a dialect of LISP designed to run on the JVM. The talk assumes some knowledge of LISP.

Part One:
Part Two:

September 25: Type-safe diff

On September 25 we discussed a paper that presents a type-safe differencing algorithm.

1 Lempsink, E., Leather, S., and Loh, A. Type-safe diff for families of datatypes. In WGP ¿09: Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming (New York, NY, USA, 2009), ACM, pp. 61¿72.

September 4, 11, October 30, November 6, 13, 20: Scala's Type System

On September 4 we read a paper that presents a core calculus for type checking the Scala programming language.

1 Cremet, V., Garillot, F., Lenglet, S., and Odersky, M. A Core Calculus for Scala Type Checking. In Mathematical Foundations of Computer Science (2006), Lecture Notes in Computer Science.

On October 30 we discussed "Generics of a Higher Kind" by Adriaan Moors et al. 1 which describes type constructor polymorphism in Scala.


On November 6 and 13 we discussed of a paper on local type inference by Pierce and Turner 1.

1 Pierce, B. C., and Turner, D. N. Local type inference. ACM Trans. Program. Lang. Syst. 22, 1 (2000), 1¿44.

On November 20 we discussed a paper about a colored version of local type inference by Odersky et. al. 1

1 Odersky, M., Zenger, C., and Zenger, M. Colored local type inference. In POPL ¿01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (New York, NY, USA, 2001), ACM, pp. 41¿53.

July 31-August 28: Pretty-Printing

On August 7, 14, 21 and 28 we discussed a paper about deriving pretty-printing combinators for a lazy functional programming language.

1 Hughes, J. The design of a pretty-printing library. In Advanced Functional Programming (1995), Springer Verlag, pp. 53¿96.

On July 31 we discussed a paper about automatically generating pretty-printers for languages.

1 van den Brand, M., and Visser, E. Generation of formatters for context-free languages. ACM Trans. Softw. Eng. Methodol. 5, 1 (1996), 1¿41.

July 24: Formal Analysis of Software Merging Schemes

Michael Olney briefed us about his nascent PhD topic.


Version control systems have become ubiquitous within the programming community. A key operation fundamental to any non-trivial version control system is that of merging divergent versions of code bases. Though there strong commonalities between the merging schemes used by the numerous systems, there is little in the way of theory describing these common concepts. A formal analysis of the different schemes used to merge source code may allow these common concepts to be transferred to types of data other than source code and directory trees. This talk will give an overview of a proposed PhD project to address this issue, and discuss some of the progress that has been made on it so far.

July 3: Program Comparison

On July 3 we will discuss "Identifying the semantic and textual differences between two versions of a program" by Horwitz.

1 Horwitz, S. Identifying the semantic and textual differences between two versions of a program. SIGPLAN Not. 25, 6 (1990), 234¿245.

June 19 and 26: Kiama

On June 19 and 26 Tony Sloane presented current work on the Kiama language processing library for Scala as a practice for an upcoming tutorial presentation.


Kiama is a lightweight language processing library for the Scala programming language. We are developing Kiama to investigate large-scale embedding of language processing methods in a modern general purpose language. This tutorial provides an overview of Kiama and examples of its use to solve typical language processing problems. Specifically, we show how to implement parsing, static analysis and transformation to implement various forms of lambda calculus. The major processing paradigms used for this task are packrat parsing, attribute grammars and strategy-based rewriting.

June 12: Datalog

On June 12 we discussed the following paper about implementing an optimising Datalog compiler.

1 Sereni, D., Avgustinov, P., and de Moor, O. Adding magic to an optimising datalog compiler. In Proceedings of the 2008 ACM SIGMOD international conference on Management of data (2008), ACM New York, NY, USA, pp. 553¿566.

June 5: Datalog

On June 5 we discussed the following paper about applying Datalog to source code analysis using an implementation based on binary-decision diagrams.

1 Whaley, J., and Lam, M. S. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI ¿04: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation (New York, NY, USA, 2004), ACM, pp. 131¿144.

May 29: Datalog

On May 29 we discussed the following paper about applying Datalog to source code querying.

1 Hajiyev, E., Verbaere, M., and de Moor, O. CodeQuest: Scalable source code queries with Datalog. ECOOP 2006 ¿Object-Oriented Programming (2006), 2¿27.

May 8, 15: Datalog

In the meetings on May 8 and 15 we discussed the paper "What you always wanted to know about Datalog (and never dared to ask)" by Ceri et al. Datalog was originally developed as way to apply the ideas from languages like Prolog in a database setting. It has more recently received attention in the programming languages community as a way to concisely specify various forms of source code analysis as inference rules.


1 Ceri, S., Gottlob, G., and Tanca, L. What you always wanted to know about Datalog (and never dared to ask). Knowledge and Data Engineering, IEEE Transactions on 1, 1 (Mar 1989), 146¿166.

March 20: Programming Languages as Communication Mechanisms

On March 20 we were delighted to host a visiting talk from Teodor Rus, Professor of Computer Science from the University of Iowa ( The talk was a general discussion of programming languages and their implementation.


Programming languages are the main tools employed by computer based problem solving processes. Yet current trends in programming language design, teaching, and use rarely relate programming languages to problem solving process. However, the lack of synchronization between increasing pervasiveness and diversity of computer technology and computer science curricula has generated concerns in the US programming language community. This talk will discuss these concerns and will analyze possible causes and feasible solutions based on speaker¿s 40 year experience in language design, implementation, and teaching. A programming language definition that integrates the three components of a programming language semantics, syntax, and pragmatics into a concept of a language will be proposed. We will also show the impact of this definition on programming language design, implementation, and use, and will discuss the feedback it may provide on the programming language curricula.

March 6: Formal Models of Version Control Systems

On March 6 we looedk at a paper that presents a formal model of version control systems.


February 27, 2009: The Isabelle Proof Assistant

On February 27 we looked at structured proofs in the Isabelle Proof Assistant.


February 20, 2009: The Isabelle Proof Assistant

On February 20 we continued looking at the Isabelle Proof Assistant. We looked at Chapter 3 of the Isabelle tutorial and Michael Olney updated us on his investigations.

February 13, 2009: The Isabelle Proof Assistant

On February 13 we started looking at the Isabelle Proof Assistant. Michael Olney took through some of his investigations. Suggested background reading on the basics of Isabelle syntax and proof construction is Chapter Two of the Isabelle tutorial.


February 6, 2009: Abstract State Machines

On February 6 we read a short introductory paper on Abstract State Machines (ASMs) which are a formal specification mechanism that generalises finite-state machines. Tony Sloane gave a demo of his implementation of ASMs in Scala using a specification of a subset of the Java Virtual Machine as an illustration.


  • No labels