Meeting 2018

• Dates: May 14-18, 2018
• Venue: Antwerp, Belgium
• Host: Tom Van Cutsem

https://lonelyplanetimages.imgix.net/mastheads/GettyImages-486812737_super.jpg

Slides

The slides of many of the talks are now available in the table at the bottom of this page.

Program

The meeting starts on Monday morning May 14th at 9AM and ends with lunch on Friday May 18th.

The program consists of a series of 50 minute sessions, which are scheduled during the meeting. In each session the speaker gets 25 minutes to present and the audience gets 25 minutes to discuss, in no particular order (although we tend to give the presenter a couple of minutes to at least introduce the topic). Time is administered using a chess clock. (If attendance is high we may have to reduce session times somewhat.)

Prospective speakers are invited to send a talk proposal including title and abstract to the chair (Eelco Visser).

Venue

The meeting will take place in Antwerp, Belgium in the offices of Nokia Bell Labs.

The offices are conveniently located right next to Antwerp Central railway station and a 10-minute walk from the city centre.

Address: Nokia Bell, Copernicuslaan 50, 2018 Antwerp, Belgium (Map). (please note: main entrance is on the Kievitplein, a pedestrian-only square, not in Copernicuslaan. The entrance is clearly marked with a big NOKIA sign.)

On the first day, please register at Reception through the main entrance (mention WGLD meeting with Tom Van Cutsem) and wait until someone comes to fetch you.

We will be meeting in Nokia building C, 11th floor, room C11-Tim Berners-Lee.

Getting There

Fly into either Brussels National Airport (BRU) or Amsterdam Schiphol Airport (AMS). Brussels is closer to the final destination, but Amsterdam has more direct long-haul flights.

From Brussels airport, the easiest option is to simply take a local train from the Brussels airport train station to Antwerp Central station. There's a direct connection that should get you from the airport into Antwerp in about 30 minutes (no upfront seat reservation required). The meeting venue is located right next to Antwerp's Central station.

From Amsterdam Schiphol airport, there is also a direct train service to Antwerp. You can either take a local commuter train (no upfront seat reservation required) which should get you there in about 2 hours, or take a high-speed train (Thalys) which will get you there in 56 minutes. Thalys trains require upfront seat reservation.

For train time tables and tickets, see the website of the Belgian national railway service NMBS.

Detailed instructions for getting to the Nokia Bell Labs Antwerp offices, including some sightseeing highlights, can be found in this leaflet.

Accommodation

The Lindner Hotel is located right next to Nokia's offices.

A block of 20 rooms has been reserved for us at discounted rates until April 15, 2018. These are economy class single rooms, at the Nokia rate of EUR 109 per night (including breakfast, excluding EUR2.39 tourist tax).

To book a room, send a mail to reservations.antwerpen@lindnerhotels.be and mention the following:

• Reservation code "WGLD", block ID. 8819749.
• Your Name
• Check-in and check-out date
• Credit card info

You will get a confirmation through e-mail.

Reservation at the discounted rates in the Lindner Hotel is possible until April 15.

An alternative option is the Leopold Hotel, just a 5-minute walk from the Nokia offices. The rate for this hotel is EUR 102 per night (including breakfast, excluding EUR2.39 tourist tax). To make a reservation, send mail to res.antwerp@leopoldhotels.com stating that you are a visitor at Nokia and would like to receive the Nokia rate.

A more budget-friendly option also within short walking distance is the Ibis Hotel Antwerp Central station. Nokia does not have a special rate, so you can just book online.

Registration

Registration is required so that we can take care of logistics. Please fill in this registration form (note: registrations are closed. Please send mail to Tom Van Cutsem to make updates to your registration)

A registration fee of EUR 250 will be due 1 month prior to the start of the meeting. This fee will cover use of the meeting room, coffee breaks Mon-Fri, lunches Mon-Fri, dinners Mon-Thu and a social event on Wed afternoon. Payment details will be sent out separately.

Schedule

Meetings will start at 9AM and end around 5-5.30PM.

Lunches and coffee breaks will be on-site.

• Monday Dinner: 6.30PM at Lindner Hotel, Lange kievitstraat 125, Antwerp (just across the street from venue)
• Tuesday Dinner: 6.30PM at Wagamama, De Keyserlei 13, Antwerp (10 minute walk from venue)
• Wednesday Dinner: 7PM at Felix Pakhuis, Godefriduskaai 30, Antwerp (30 minute walk from venue, or take bus)
• Thursday Dinner: 7PM at Gran Duca, De Keyserlei 28, Antwerp (10 minute walk from venue)

Participants

Organizers

• Tom van Cutsem (local organizer)
• Eelco Visser (chair)
• Tijs van der Storm (vice-chair)
• Jonathan Edwards (secretary)

Members

• William Cook
• Klaus Ostermann
• Markus Voelter
• Roberto Ierusalimschy
• Jan-Willem Maessen
• Luke Church
• Edwin Brady
• Andrew Black
• James Noble
• Erik Ernst
• Klaus Ostermann

Visitors

• Nada Amin
• Matthias Hauswirth
• Éric Tanter
• Ronald Garcia
• Jan Vitek
• Stefan Marr
• François Pottier
• Elisa Gonzalez Boix
• Sylvan Clebsch

Program

Monday

• Jonathan Edwards
• Roberto Ierusalimschy
• Eelco Visser

• Tijs van der Storm
• Markus Voelter
• Andrew Black

Tuesday

• Jan Vitek
• Ronald Garcia
• Stefan Marr

• Francois Pottier
• Eric Tanter
• Matthias Hauswirth

Wednesday

• Klaus Ostermann
• Sylvan Clebsch
• William Cook

Excursion in the afternoon

Thursday

• Elisa Gonzalez Boix
• Jan-Willem Maessen
• Luke Church

• Nada Amin
• Erik Ernst
• Business Meeting

Friday

• Tom van Cutsem
• James Noble

Talk abstracts

Markus Voelter: A spreadsheet extension for KernelF

As we all (sometimes slightly jealously) acknowledge, spreadsheets are used widely for "programming", especially by the domain-experts we often want to convince of DSLs. We also all agree about the limitations of spreadsheets in terms the error-proneness of large, intricate sheets.

Essentially, spreadsheets represent functional programs that are executed reactively, whenever a user changes the contents of a cell. This makes them fit well with functional programming in general.

In this talk I present a prototypical extension of the KernelF^? functional programming language that supports spreadsheets. I briefly introduce KernelF^?, discuss the motivation for building the spreadsheet extension and then demonstrate how it fits in with KernelF^?'s functional paradigm.

We have also made several extensions of the spreadsheet paradigm that aim at fixing some of the problems observed in spreadsheets. I will introduce those, and hope to get feedback on other ideas we could

Eelco Visser: The Syntax Definition Formalism SDF3

I describe the design of the syntax definition formalism SDF3 by means of propositions that capture its concepts.

Andrew P. Black: Design Principles for 
the Grace AST

Grace dialects can restrict the dialectic language by writing a tree-walker for the AST that restricts allowable programs (compared to standard Grace). As a consequence, the Grace language definition must include a definition of an AST for Grace.

What are the requirements on such an AST? Can we come up with “Design Principles” for an AST to guide us in its design? How do we know when the AST is adequate? Or when it is overspecified? What is an AST, anyway?

Now that there are multiple implementations of Grace, it is time to face these questions. I don’t have many answers, but hope that the combined expertise of the working group will help us find some.

Roberto Ierusalimschy: The Titan Programming Language

The Titan Programming Language: a statically typed companion language to Lua, designed for writing applications and libraries, with performance in mind.

Jonathan Edwards: Direct Programming

To make programming more concrete I am taking another run at the old ideas of macro recording and Programming by Example. Many such efforts abstracted user actions into conventional code. Instead I co-design the PL and UI to be analogous, so that programs and users have the same capabilities, and programs look much like recorded transcripts of user actions. This correspondence may aid beginning programmers. Another benefit is that programs can not only be abstracted from user actions but also be incrementally revised through further actions.

Any attempt to make programming more concrete must overcome two main obstacles: loops and conditionals, for they deal with hypothetical situations. My approach is to extend the direct manipulation metaphor onto template states that prototype iteration, and example states that witness alternative cases.

Jan Vitek: The Beauty and the Beast — from Fortress to Julia

Take two languages, Julia and Fortress, designed to solve similar problems with similar mechanisms and compare the approaches that led to one to being adopted and the other discontinued. What lessons are there for language designers? Can the designs be reconciled? Can we somehow turn the beast that is into the beauty that could have been? This talk is a snapshot of our investigations into Julia with more open questions than definitive answers. Julia’ design is a pragmatic effort driven by use-cases and user feedback. In contrast, Fortress followed a principled, formally grounded, approach that aimed for type soundness first. We will marvel at the efficacy of Julia's compiler -- a one-trick pony that works well in practice. We will inspect the multi-dispatch feature of Julia and puzzle at the subtype relation that is at its heart. The takeaway of the talk is a list of language features that are key to performance and usability.

Ronald Garcia: Type-driven Gradual Security Typing

Information-flow security-typed programming languages use types to statically enforce noninterference between potentially conspiring values, such as the arguments and results of functions. But to adopt static security types, like other advanced type disciplines, programmers must adopt the discipline wholesale.

To provide a gentler path to security typing, researchers have designed languages that blend static and dynamic checking of security types. Unfortunately most of these languages support static, type-based reasoning about noninterference if programs are entirely statically secured. This limitation substantially weakens the benefits that dynamic enforcement brings to static security typing.

This talk describes GSLref, a security-typed higher-order language that supports gradual migration between a simple type discipline and security type discipline, using the principles underlying gradual typing.

GSLref satisfies most of the criteria set forth by Siek et al. for gradually-typed languages. The one exception, called the "dynamic gradual guarantee" cannot be satisfied without violating noninterference.

To realize this design, we were led to draw a sharp distinction between syntactic type safety and semantic type soundness, each of which constrains the design of the gradual language.

Stefan Marr: Designing Small and Versatile Collection Libraries: Providing an Efficient and Thread-Safe Implementation

Collection libraries differ significantly between languages, but there are some indications that we could make do for most use cases simply with sequence, map, and set collections. Modern dynamic languages show this form of minimalism and compensate by making their collections highly versatile. For instance, an array is usually dynamically sized and provides operations to act as queue, dequeue, or stack. However, this design comes with implementation challenges and dynamic language implementations apply various optimizations to make it efficient.

So far, these optimizations have been one of the reasons that languages such as Ruby and Python do not yet have implementations that are efficient and allow parallel execution while providing a thread-safe implementation that does not expose any races from the VM implementation to the language.

This talk presents a technique to ensure implementation-level thread-safety for such collections. With it, we enable an idiomatic dynamic language programming style for parallel code. In practice this means, VMs do not need a global interpreter lock to guarantee safety while avoiding to compromise single-threaded execution performance.

Matthias Hauswirth: Misconceptions & PL Design

Programming languages are conceptually dense constructions. Expressing a program in a given language requires an accurate understanding of the concepts of that language. A programmer’s misconceptions about a language eventually lead to incorrect programs.

In this talk I will give a brief introduction to an area of the learning sciences focusing on human conceptions, misconceptions, and conceptual change. I will then try to connect these ideas to programming language design. My goal with this talk is to trigger discussions on PL design and evaluation by stepping outside the normal PL design zone.

Klaus Ostermann: Dualizing Generalized Algebraic Data Types by Matrix Transposition

We characterize the relation between generalized algebraic datatypes (GADTs) with pattern matching on their constructors one hand, and generalized algebraic co-datatypes (GAcoDTs^?) with copattern matching on their destructors on the other hand: GADTs can be converted mechanically to GAcoDTs^? by refunctionalization, GAcoDTs^? can be converted mechanically to GADTs by defunctionalization, and both defunctionalization and refunctionalization correspond to a transposition of the matrix in which the equations for each constructor/destructor pair of the (co-)datatype are organized. We have defined a calculus, GADT^T, which unifies GADTs and GAcoDTs^? in such a way that GADTs and GAcoDTs^? are merely different ways to partition the program.

We have formalized the type system and operational semantics of GADT^T in the Coq proof assistant and have mechanically verified the following results: 1) The type system of \ourlang{} is sound, 2) defunctionalization and refunctionalization can translate GADTs to GAcoDTs^? and back, 3) both transformations are type- and semantics-preserving and are inverses of each other, 4) (co-)datatypes can be represented by matrices in such a way the aforementioned transformations correspond to matrix transposition, 5) GADTs are extensible in an exactly dual way to GAcoDTs^?; we thereby clarify folklore knowledge about the ``expression problem''.

We believe that the identification of this relationship can guide future language design of ``dual features'' for data and codata.

This talk is based on joint work with Julian Jabs.

Eric Tanter: Gradual Parametricity, Revisited

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated almost a decade ago, and several recent developments have been published in the past year. On the one hand, the different forces at play have led researchers to propose language designs with varying goals and compromises, with sometimes surprising consequences. On the other hand, the complexity of the technical details has resulted in several important results to remain stated as conjectures. In this work, we first identify a crucial, yet ignored, property of a language with gradual parametricity, which turns out to be violated by all prior work. This observation suggests that existing cast calculi are not well suited for supporting a gradual version of System F. We then formulate clear design goals for a gradual language with explicit parametric polymorphism, GSF, and explore to which extent the Abstracting Gradual Typing methodology helps us derive such a language. GSF satisfies all the expected properties, save for one property—the dynamic gradual guarantee—which was left as conjecture in all prior work. Here, we prove that this property is simply incompatible with parametricity, unless one is willing to adjust accepted definitions. This situation, reminiscent of recent results on gradual noninterference, reinforces the view that new criteria might be needed to characterize the spectrum of type-based reasoning that gradual typing supports when applied to semantically-rich disciplines.

William Cook: Rethinking Excel in Enso

I’m trying to rethink Excel to eliminate repeated but slightly different equations, and have a secure approach to editing rows and columns, so that equations are always correctly defined. I have two sample Excel applications: one involving grades (normalizing them, curving them, combining them, etc), and one involving work scheduling, but the idea changing Excel to have a Data Model, Computation Model, and a Presentation model, is generally appealing. The question is how to design the modeling languages to work together and implement an engine that can let users view the models as a grid (or other views), while editing at multiple different levels. I need some help with my presentation model.

Luke Church: Entangling intelligences

I present work at Lark Systems, integrating together different types of thinking and the way these affect the way people program.

Francois Pottier

Reachability and error diagnosis in LR(1) parsers

Contrary to an ill-advised folklore myth, an LR(1) parser can produce good syntax error messages. In fact, an LR(1) parser generator can build a collection of erroneous input sentences that covers every “error state”, that is, every state of the LR automaton in which an error might be detected. This feature can be exploited by a grammar designer to examine each such state and either (a) propose a handwritten diagnostic message for this state, or (b) modify the grammar and/or the automaton so that this error state disappears. I report on an application of this technique to the CompCert^? ISO C99 parser, and discuss its strengths and limitations. (This work was presented at CC 2016.)

and the visitors talk:

Visitors Unchained

Traversing and transforming abstract syntax trees that involve name binding is notoriously difficult to do in a correct, concise, modular, customizable manner. I address this problem in the setting of OCaml, a functional programming language equipped with powerful object-oriented features, using visitor classes as partial, composable descriptions of the operations that we wish to perform on abstract syntax trees. (This work was presented at ICFP 2017.)

Sylvan Clebsch: Language Runtimes for Parallel Programming: Weak Memory and Program Order

Language runtimes notoriously involve frantic bit twiddling, very fine grained atomic operations, and a reliance on the specific behaviour of particular architectural targets. How do we know our code implements our intended memory model? How do we know our memory model maps, and maps efficiently, to the hardware memory model? What is “program order” when we need interleaved and independent “happens before” guarantees? What is the type of a range of memory reserved by the memory allocator before it has been committed, or after it has been freed by the language? Perhaps we need a low-level systems language for writing runtimes that treats “happens before” as a core building block.

Jan-Willem Maessen: Confessions of a Reluctant Imperative Programmer

I consider myself a functional programmer who happens to do a lot of systems programming in non-functional languages. But the imperative style of control flow – loops with break and continue, functions with intermediate return, local variables that can be re-bound – is in many cases easier for me as a programmer to read and write than the equivalent code in a typical functional language. Why is this? And when does it break down? I'll end with some questions about how we might do better.

Tom van Cutsem: Control flow goodness in modern JavaScript^?

A whirlwind tour of JavaScript^?’s most recently added control flow constructs: promises, iterators, generators and async functions.