Reading Group Archive (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.
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"https://google.com" 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.
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.
Pretty-Printing
On June 2 we discussed the (draft) paper The Final Pretty Printer by Christiansen et al.
Clojure
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.
F*
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.
LiquidHaskell
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.