Informal minutes of IFIP Working Group 2.8
27th meeting, Shirahama, Japan
April 11-16, 2010

List of attendees

Members: Lennart Augustsson Olivier Danvy Kathleen Fisher Fritz Henglein John M. Hughes Mark P. Jones John Launchbury David B. MacQueen Rishiyur S. Nikhil Simon Peyton Jones Didier Remy Colin Runciman Mary Sheeran Satnam Singh Peter Thiemann

Observers: Kenichi Asai Kung Chen Jacques Garrigue Zhenjiang Hu Atsushi Igarashi Naoki Kobayashi Sean McDirmid Yasuhiko Minamide Keiko Nakata Atsushi Ohori Sungwoo Park Sukyoung Ryu Eijiro Sumii

Note: many of the links are dead, which simply means that I haven't yet received the material.

Technical presentations

Satnam Singh, Synthesis of Data-Parallel GPU Software into GPU code, Multicore Software and FPGA Hardware. (Mon 2010-04-12, 09:30-10:00)

This presentation introduces an embedded domain specific language (DSL) called Accelerator for data-parallel programming which can target GPUs, SIMD instructions on x64 multicore processors and FPGA circuits. This system is implemented as a library of data-parallel arrays and data-parallel operations with implementations in C++ and for .NET languages like C#, VB.NET and F#. We show how a carefully selected set of constraints allow us to generate efficient code or circuits for very different kinds of targets. Finally we compare our approach which is based on JIT-ing with other techniques e.g. CUDA which is an off-line approach as well as to stencil computations. The ability to compile the same data parallel description at an appropriate level of abstraction to different computational elements brings us one step closer to finding models of computation for heterogonous multicore systems.

Atsushi Ohori, An Efficient Bitmap Marking Garbage Collector for Functional Languages. (Mon 2010-04-12, 10:00-10:45)

Rishiyur S. Nikhil, Programming Problem: A programming/specification and verification problem based on the Intel QPI protocol (QuickPath Interconnect). (Mon 2010-04-12, 11:00-11:10)

QPI is Intel's new interconnect network for multiprocessors. It consists of high-speed point-to-point links that connect processors, caches, memories, and I/O devices (published in a book by Intel). Here, we describe the "Link Layer" of the QPI protocol, embodying concurrency and error recovery. The questions for the WG 2.8 audience are: How would you formalize this in a programming language or specification language of your choice? How would you prove correctness properties about it?

Olivier Danvy, Programming Problem: Write a CPS version of append. (Mon 2010-04-12, 11:10-11:20)

Simon Peyton Jones, Programming Problem: Termination Puzzle from CACM. (Mon 2010-04-12, 11:20-11:30)

Communications of the ACM Vol. 52 No. 2, Page 104 10.1145/1461928.1461952.

Research Problems, Discussion. (Mon 2010-04-12, 11:30-12:30)

Naoki Kobayashi, Higher-Order Model Checking. (Mon 2010-04-12, 14:00-14:45)

The talk gives an overview of a series of our recent work on higher-order model checking and its applications to program verification. We first introduce higher-order model checking (more precisely, model checking of higher-order recursion schemes) and show how verification problems for higher-order functional programs can be reduced to the higher-order model checking. We then show how the higher-order model checking can be reduced to the type checking problem for an intersection type system. Based on the reduction, we have implemented TRecS, the first model checker for higher-order recursion schemes, which is reasonably first despite the extremely high worst-case complexity of the model checking problems. We conclude the talk by discussing ongoing and future work to construct software model checkers for higher-order functional programs on top of the higher-order model checker.

Kenichi Asai, A Reinvestigation of Filinski's Symmetric Lambda Calculus. (Mon 2010-04-12, 14:45-15:30)

In this talk, I present a symmetric lambda calculus (SLC) in which both the duality between call-by-value and call-by-name and the duality between expressions and continuations hold at the same time. The idea of SLC was originally introduced by Filinski in 1989, but has not been investigated seriously since then. Here, I reformulate SLC using small-step reduction semantics and show various examples. The type system for SLC naturally corresponds to classical logic. At the end of the talk, I speculate on what kind of programming we can do based on classical logic.

Keiko Nakata, Lazy Modules. (Tue 2010-04-13, 09:00-09:45)

I investigate evaluation strategies for ML-style modules supporting recursion. I am particularly interested to find a happy compromise between call-by-value and lazy strategies, as inspired by Syme's initialization graphs. I formalize hybrid strategies between call-by-value and lazy, with different degrees of laziness, by translating a source syntax for modules into target languages, which are very much inspired by Felleisen and Hieb's call-by-value lambda calculus with state and Ariola and Felleisen's call-by-need cyclic lambda calculus. Different strategies are expressed by tweaking the translation as well as the operational semantics of the target languages.

Atsushi Igarashi, Self Type Constructors. (Tue 2010-04-13, 09:45-10:30)

Bruce and Foster proposed the language LOOJ, an extension of Java with the notion of MyType, which represents the type of a self reference and changes its meaning along with inheritance. MyType is useful to write extensible yet type-safe classes for objects with recursive interfaces, that is, ones with methods that take or return objects of the same type as the receiver. Although LOOJ has also generics, MyType has been introduced as a feature rather orthogonal to generics. As a result, LOOJ cannot express an interface that refers to the same generic class recursively but with different type arguments. This is a significant limitation because such an interface naturally arises in practice, for example, in a generic collection class with method map(), which converts a collection to the same kind of collection of different elements. Altherr and Cremet and Moors, Piessens, and Odersky gave solutions to this problem but they used a highly sophisticated combination of advanced mechanisms such as abstract type members, higher-order type constructors, and F-bounded polymorphism. In this talk, we give another solution by introducing self type constructors, which integrate MyType and generics so that MyType can take type arguments in a generic class. Our solution is simpler - it uses only first-order type constructors and neither abstract type members nor F-bounds. We demonstrate the expressive power of self type constructors by means of examples, formalize a core language with self type constructors, and prove its type safety.

Sean McDirmid, CloudTalk: Programming with Search and Wikis. (Tue 2010-04-13, 11:00-11:45)

Jacques Garrigue, Certifying OCaml type inference (and other type systems). (Tue 2010-04-13, 14:00-14:45)

The type system of Objective Caml has many unique features, which make ensuring the correctness of its implementation difficult. One of these features is structurally polymorphic types, such as polymorphic object and variant types, which have the extra specificity of allowing recursion. I implemented in Coq a certified interpreter for Core ML extended with structural polymorphism and recursion. Along with type soundness of evaluation, soundness and principality of type inference were proved too. In contrast with these difficult proofs, I also proved a substitution lemma for a path rewrite calculus modelling recursive modules. While the lemma is hard to prove on paper, its formalization was not so difficult, thanks to a clever way to avoid binders in the calculus.

Sukyoung Ryu, Project Fortress, from SunLabs to KAIST. (Tue 2010-04-13, 14:45-15:30)

Fortress is a new programming language designed for High Performance Computing with high programmability. It provides mathematical syntax to enable scientists and engineers to write their programs in their own language. It also provides built-in support for easy and correct parallel programming. Moreover, its macro system allows for the language growth by extending the syntax and semantics of Fortress. Project Fortress started under the Sun/DARPA HPCS program from 2003 through 2006, and it has been open-sourced with international participation since 2007. Now that the presenter, used to be the Lead Author of the Fortress language specification and the Lead Developer of the Fortress compiler front end, moved from Sun Labs to KAIST, this talk presents slightly different research directions at an industrial lab and an academia. As an example of formalization efforts for Fortress, this talk describes modular multiple dispatch mechanism supporting multiple inheritance.

Kung Chen, Side-Effect Localization for Lazy, Purely Functional Languages via Aspects. (Tue 2010-04-13, 16:00-16:45)

Many side-effecting programming activities, such as profiling and tracing, can be formulated as crosscutting concerns and be framed as side-effecting aspects in aspect-oriented programming paradigm. The benefit gained from this separation of concern is particularly evident in purely functional programming, as adding such aspects using techniques such as monadification will generally lead to crosscutting changes. This talk presents an approach to provide side-effecting aspects for purely lazy functional languages in a user transparent fashion. We propose a simple yet direct state manipulation construct for developing side-effecting aspects and devise a systematic monadification scheme to translate the woven code to a purely monadic style functional code. Furthermore, we present a static and dynamic semantics of the aspect programs and reason about the correctness of our monadification scheme with respect to them.

Yasuhiko Minamide, The PHP String Analyzer. (Wed 2010-04-14, 09:00-09:45)

We developed a program analyzer for PHP that approximates the string output of a program with a context-free grammar. By applying the analysis to a server-side program, dynamically generated Web pages can be approximated with a context-free grammar. The approximation obtained by the analysis has many applications in checking the validity and security of a server-side program. It is successfully applied to publicly available PHP programs to check the validity of dynamically generated pages. Wassermann and Su extended the analyzer to detect SQL injection and cross-site scripting vulnerabilities.

John Launchbury, Orchestrating Concurrent Systems (and Scripts). (Wed 2010-04-14, 09:45-10:15)

Zhenjiang Hu, Can Graph Transformation be Bidirectionalized? (Wed 2010-04-14, 10:45-11:30)

Bidirectional transformations provide a novel mechanism for synchronizing and maintaining the consistency of information between input and output. Despite many promising results on bidirectional transformations, these have been limited to the context of relational or XML (tree-like) databases. We challenge the problem of bidirectional transformations within the context of graphs, by proposing a formal definition of a well-behaved bidirectional semantics for UnCAL, i.e., a graph algebra for the known UnQL graph query language. The key to our successful formalization is full utilization of both the recursive and bulk semantics of structural recursion on graphs. We carefully refine the existing forward evaluation of structural recursion so that it can produce sufficient trace information for later backward evaluation. We use the trace information for backward evaluation to reflect in-place updates and deletions on the view to the source, and adopt the universal resolving algorithm for inverse computation and the narrowing technique to tackle the difficult problem with insertion. We prove our bidirectional evaluation is well-behaved. Our current implementation is available online and confirms the usefulness of our approach with nontrivial applications. Reference: Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Keisuke Nakano, Kazutaka Matsuda, Bidirectionalizing Graph Transformations, 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), Baltimore, Maryland, USA, September 27-29, 2010.

Peter Thiemann, Contracts and Laziness. (Wed 2010-04-14, 11:30-12:00)

Contract monitoring for strict higher-order functional languages has an intuitive meaning, an established theoretical basis, and a standard implementation. For lazy functional languages, the situation is less clear-cut. There is no agreed-upon intended meaning or theory, and there are competing implementations with subtle semantic differences. We propose meaning preservation and completeness as formally defined properties for evaluating implementations of contract monitoring. A survey of existing implementations reveals that some are meaning preserving, some are complete, and some have neither property. The main result is that contract monitoring for lazy functional languages cannot be complete and meaning preserving at the same time, although both properties can be achieved in isolation. A similar choice between completeness and meaning preservation is present at the level of functions and the paper proposes a novel approach to increase completeness for functions. With this approach, a novel, complete implementation can be constructed.

Eijiro Sumii, Environmental Bisimulation. (Thu 2010-04-15, 09:00-09:45)

I present environmental bisimulations, a proof method for program equivalence in a wide variety of languages, including a polymorphic lambda-calculus with higher-order store, and a higher-order pi-calculus with cryptographic primitives.

Dave MacQueen, Higher-order Modules. (Thu 2010-04-15, 09:45-10:15)

Research Problems, Introduction. (Thu 2010-04-15, 10:45-11:15)

Keiko Nakata,

We are seeking a model for a call-by-need letrec calculus, which distinguishes direct cycles, such as let rec x = x in x, let rec x = y, and y = x + 1 in x, and looping recursion, such as let rec f = \x . f x in f 0.

Fritz Henglein, Kleene Meets Church - Regular Expressions as Types (Thu 2010-04-15, 11:15-11:45)

We show that regular expression containment can be characterized by the existence of a certain class of functions between the regular expressions interpreted as types. Since they correspond to transformations on syntax trees under regular expressions understood as a grammar, they have also have practical significance since regular expressions are often used for extracting parts from input, not just provide yes/no answers. We provide a sound and complete coinductive axiomatization of regular expression containment, whose computational interpretation yields coercions and thus provides a computational interpretation of containment proofs as syntax tree transformers. We discuss possible conceptual and practical applications of understanding regular expressions as types and containment proofs as code for coercions. The include parametric completeness, synthesis of efficient coercions, oracle coding (regular-expression specific coding of strings), fast parsing, ambiguity resolution, and regular expressions as refinement types for strings.

Olivier Danvy, A Syntac Theory of Combinatory Graph Reduction. (Thu 2010-04-15, 11:45-12:15)

Research Problems, Working. (Thu 2010-04-15, 14:00-17:00)

Mark Jones, Developing Good Habits for Bare-Metal Programming. (Thu 2010-04-15, 17:00-17:30)

Lennart Augustsson, "Re-opening closures" reopened. (Thu 2010-04-15, 17:30-18:00)

Rishiyur S. Nikhil, Two uses of FP techniques in HW design. (Fri 2010-04-16, 09:00-09:30)

We describe two uses of functional programming in hardware desgn, embodied in the language BSV (Bluespec SystemVerilog). (1) PAClib (Pipeline Architecture Constructor Library), a collection of higher-order functions for flexible and compositional descriptions of pipelined architectures. (2) Using monads to hide all the "plumbing" necessary to implement Signal Probes from arbitrary points deep within a hardware module hierarchy.

John Hughes, Solution: The QPI problem. (Fri 2010-04-16, 09:30-09:40)

Simon Peyton Jones, Solution: Termination Puzzle. (Fri 2010-04-16, 09:40-09:50)

Communications of the ACM Vol. 52 No. 3, Page 111 10.1145/1467247.1467272.

Simon Peyton Jones, Using Type Functions in Dataflow Optimization. (Fri 2010-04-16, 10:30-11:00)

Dataflow analysis and transformation of control-flow graphs is pervasive in optimizing compilers, but it is typically entangled with the details of a particular compiler. We describe Hoopl, a reusable library that makes it unusually easy to define new analyses and transformations for any compiler written in Haskell. Hoopl's interface is modular and polymorphic, and it offers unusually strong static guarantees. The implementation encapsulates state-of-the-art algorithms (interleaved analysis and rewriting, dynamic error isolation), and it cleanly separates their tricky elements so that they can be understood independently.

John Launchbury, More Orc. (Fri 2010-04-16, 11:00-11:30)

Kenichi Asai, Typed Printf via Delimited Continuations, Functional Pearl. (Fri 2010-04-16, 11:30-12:00)

In this talk, I describe how a type-safe printf can be implemented succinctly using delimited continuations. The key observation is that % changes the type of its context. I show a demo using a caml light system extended with delimited continuation constructs, shift and reset.

John Hughes, Unit Testing. (Fri 2010-04-16, 12:30-13:00)