Reading Group Archive (2009)
Program Obfuscation
On December 4 we discussed a paper and accompanying web page on the issue of whether program obfuscation is possible. This was the final meeting for 2009.
Go
On November 27 we watched an overview talk about the new Go programming language.
Clojure
On October 9 and 23 we watched a talk (part one, part two) 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.
Type-safe diff
On September 25 we discussed a paper that presents a type-safe differencing algorithm.
Scala's Type System
On November 20 we discussed a paper about a coloured version of local type inference by Odersky et. al.
On November 6 and 13 we discussed a paper on local type inference by Pierce and Turner.
On October 30 we discussed Generics of a Higher Kind by Adriaan Moors et al. which describes type constructor polymorphism in Scala.
On September 4 we read a paper that presents a core calculus for type checking the Scala programming language.
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.
Formal Analysis of Software Merging Schemes
Michael Olney briefed us about his nascent PhD topic.
Abstract
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.
Program Comparison
On July 3 we will discuss Identifying the semantic and textual differences between two versions of a program by Horwitz.
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.
Abstract
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.
Datalog
On June 12 we discussed the paper about implementing an optimising Datalog compiler.
On June 5 we discussed the paper about applying Datalog to source code analysis using an implementation based on binary-decision diagrams.
On May 29 we discussed the paper about applying Datalog to source code querying.
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). 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.
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. The talk was a general discussion of programming languages and their implementation.
Abstract
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 analyse 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.
Formal Models of Version Control Systems
On March 6 we looked at a paper that presents a formal model of version control systems.
The Isabelle Proof Assistant
On February 27 we looked at structured proofs in 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.
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.
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.