We are proud announce our keynote speakers for APLAS’20:

Luca Cardelli, University of Oxford

Title of Talk: Integrated Scientific Modeling and Lab Automation

The cycle of observation, hypothesis formulation, experimentation, and falsification that has driven scientific and technical progress is lately becoming automated in all its separate components. However, integration between these automated components is lacking. Theories are not placed in the same formal context as the (coded) protocols that are supposed to test them: neither description knows about the other, although they both aim to describe the same process. We develop integrated descriptions from which we can extract both the model of a phenomenon (for possibly automated mathematical analysis), and the steps carried out to test it (for automated execution by lab equipment). This is essential if we want to carry out automated model synthesis, falsification, and inference, by taking into account uncertainties in both the model structure and in the equipment tolerances that may jointly affect the results of experiments.

Hidehiko Masuhara

Title of Talk: Object Support for GPU Programming: Why and How

General-purpose computing on graphics processing units (GPGPU) is now widely used in many application domains. However, programming for GPGPU is challenging due to its peculiar performance characteristics and still being done either in low-level languages or through libraries (e.g., those for matrix computation and machine learning). This talk discusses the performance challenges of using objects in GPGPU programming from the viewpoint of memory management, and the efficient mechanisms to support objects.

Nadia Polikarpova

Title of Talk: Generating Programs from Types

Program synthesis is a promising approach to automating low-level aspects of programming by generating code from high-level declarative specifications. But what form should these specifications take? In this talk I will advocate for using types as input to program synthesis. Types are widely adopted by programmers, they can vary in expressiveness and capture both functional and non-functional properties, and finally, type checking is often fully automatic and compositional, which helps the synthesizer find the right program.

I will describe two type-driven program synthesizers we developed. The first one is Synquid, a synthesizer for recursive functional programs that uses expressive refinement types as a specification mechanism. The second one is Hoogle+, which relies on more mainstream Haskell types and generates code snippets by composing functions from Haskell libraries.