Reading Group Archive (2019)
Information-flow Control in Programming Languages
On November 29, we discussed the paper MAC A verified static information-flow control library by Vassena et al from the Journal of Logical and Algebraic Methods in Programming.
The Cooma Programming Language
On September 27, Tony Sloane presented an overview and demo of the Cooma programming language that is being designed and implemented in the PLV group. Cooma is based on a simple version of object capabilities and is being used as a platform for investigating secure language design.
Extensible data types
On September 20 we discussed the paper Abstracting extensible data types: or, rows by any other name by Morris and McKinna from POPL 2019.
Secure Programming Languages
On July 26 we discussed the paper What is a Secure Programming Language? by Cristina Cifuentes and Gavin Bierman from SNAPL 2019.
Continuations
On July 5 and 12 we discussed the paper Functional semantics of parsing actions, and left recursion elimination as continuation passing by Hayo Thielecke from PPDP 2012.
On June 28 Cameron Pappas presented a short talk that introduced continuations and their use in compilation.
Abstract
Continuations have a number of applications in both programming language theory and compiler construction. A common use for continuations is to use them to define intermediate languages in compilers that have an explicit control flow. In this talk we will present our findings on continuations and present a simple continuation passing style compiler.
The JastAdd Attribute Grammar System
On June 7 Dr Niklas Fors presented the JastAdd system which has been developed by his group at Lund University.
JastAdd is a tool for writing declarative and extensible software language specifications. It is based on Reference Attribute Grammars (RAGs), which is a formalism for decorating trees with computed properties defined by equations. RAGs extend Knuth's Attribute Grammars with references, allowing graphs to be computed on top of the tree, which is useful for several static analyses. JastAdd has successfully been used to implement compilers for several languages, including Java and Modelica. This talk gives an introduction to attribute grammars and JastAdd, and some of its applications.
Map Invariants for Program Verification
On March 22 we discussed the paper The Map Equality Domain by Dietsch et al.
Skink Language Server
On March 15, Tony Sloane updated the group on progress toward building a Language Server for our Skink verification tool. We discussed what language servers are, what they can provide, our extensions to the basic framework, and how we are integrating Skink into the framework.
UPPAAL Model Checker
On February 22 we discussed the UPPAAL model checker, based on an introductory tutorial chapter by Vaandrager.
Abstract Interpretation
On February 15 we discussed the paper Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT by Jiang et al from VMCAI 2017.
Coding Session
On February 8 we got together to help each other with current coding projects. Bring your current work and join us.
Algebraic Effects and Handlers
On February 1 we discussed the paper An Introduction to Algebraic Effects and Handlers by Matija Pretnar.
Language Server Protocol
On January 18 we discussed Microsoft’s Language Server Protocol which is designed to provide efficient communication between front-ends such as text editors and language-specific services.
Tony Sloane also described and demo some work in progress to add language server support to Macquarie’s Kiama language processing library.