Reading Group Archive (2013)
Socio-PLT
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 discussed two early papers about using path expressions to coordinate concurrent processes:
- Path Expressions by Habermann, and
- Predicate Path Expressions by Andler
Language Support for Component Life-Cycles
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 life-cycle
- enforcing correct usage of program components through their usage life-cycle
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 life-cycle
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.
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 23 and 30 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 demonstrations 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, and one by Sean McDermid on live programming research at Microsoft. 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 cyber-physical 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.
Kiama
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.
Idris
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.
Iteratees
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
On May 24 Len Hamey gave us an update on his current work to extend the Halide image processing library.
On March 8 we continued our discussion from March 1, particularly discussing how the Halide image processing language uses the LLVM framework.
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 February 22 after a brief introduction from Len Hamey, we discussed a paper about the halide language.
Early DSL's in this area used procedural programming style and focused on automatic parallelization 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 pre-compiled. Halide programs are at least as efficient as hand tuned algorithms. Back-ends target Intel architecture, ARM and CUDA with parallelization and SSE vectorization.
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 speed-ups.
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.