Reading Group Archive (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.
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 ecosystem. Scala has traditionally relied on combinator libraries 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 provides 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.
Idris
On September 16, 23 and 30 we discussing the paper Idris, a general-purpose dependently typed programming language: Design and implementation by Edwin Brady.
PureScript
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 demonstrations 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.
Effects
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
Abstract 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.