This page lists the past topics of the Programming Languages Reading Group.
Note: topics are listed in reverse chronological order.
Topics from 2017
Type Systems as Macros
On May 19 we discussed the paper “Type systems as macros” by Chang et al that appeared at POPL 17.
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.
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.
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.
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 deﬁning 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 deﬁnition notation that incorporates annotations for tree construction and pretty-printing. As well as generating a Rats! grammar, sbt-rats can optionally generate case class deﬁnitions for the tree structure and a pretty-printer deﬁned using our Kiama language processing library. We explain the sbt-rats gram- mar notation and describe our positive experiences using it to deﬁne 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 August 19 and September 2 we discussed the paper "An Abstract Memory Functor for Verified C Static Analysers" that will appear at ICFP 2016.
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.
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
Beyond Roles at Runtime
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.
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.
On May 15 we will discuss the paper Refinement of Trace Abstraction by Heizmann et al.
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
On March 20, we discussed an old paper by Tony Hoare on programming language design.
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.
Topics from 2014
Flow Fusion for the Biggest Data
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.
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.
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).
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 22 we discussed a paper from POPL 2012 about mechanisation of semantic models in the Racket language.
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 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 , 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 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.
On April 12, we discussed the SPLASH Onward! 2010 paper Pure and declarative syntax definition: paradise lost and regained by Kats and Visser.
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 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.
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.
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 14, we discussed the CoffeeScript language, based on the language documentation.
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.
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.
- 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.
- 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.
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.
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.
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 http://phoenix.inria.fr/charles-consel)
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.
1 A FORMALIZATION OF DARCS PATCH THEORY USING INVERSE SEMIGROUPS
Topics from 2010
On December 17 we looked at the [Clang C/C++/Objective-C front-end":http://clang.llvm.org/ 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:
http://augustss.blogspot.com/2009/01/llvm-llvm-low-level-virtual-machine-is.html http://augustss.blogspot.com/2009/01/llvm-arithmetic-so-we-want-to-compute-x.html http://www.serpentine.com/blog/2008/01/03/llvm-bindings-for-haskell/
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.
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.
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.
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.
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.
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.
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
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
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.
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.
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
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.
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.
Topics from 2009
December 4: Program Obfuscation
1 On the (Im)possibility of Obfuscating Programs, Barak, et. al., Crypto 2001, http://www.springerlink.com/content/telalqdcx3n600uf/
November 27: Google's Go language
On November 27 we watched an overview talk 1 about Google's new Go programming language.
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.
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.
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.
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.
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 (http://www.cs.uiowa.edu/~rus/). 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.
- 1 Chapter Two of Nipkow, T., Paulson, L. C., and Wenzel, M. A Proof Assistant for Higher-Order Logic. Springer-
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.
- 1 Gurevich, Y. Abstract state machines: An overview of the project. In Foundations of Information and Knowledge Systems (2004), Springer-Verlag, pp. 6¿13.