FLOPS 2018 Program


9 May, Wednesday

8:30 Registration opens

9:25 Welcome

9:30 Invited talk (1h00)

10:30 Coffee Break (0h30)

11:00 Session I (1h30)

12:30 Lunch (2h00)

14:30 Session II (1h00)

15:30 Coffee Break (0h30)

16:00 Session III (1h00)

10 May, Thursday

9:30 Invited talk (1h00)

10:30 Coffee Break (0h30)

11:00 Session IV (1h30)

12:30 Lunch (2h00)

14:30 Session V (1h00)

15:30 Coffee Break (0h30)

16:00 Session VI (1h00)

17:15 Buses depart for banquet

18:15 Banquet

11 May, Friday

9:30 Invited talk (1h00)

10:30 Coffee Break (0h30)

11:00 Session VII (1h30)

Abstracts for Invited Talks

miniKanren: a Family of Languages for Relational Programming

William E. Byrd (University of Alabama at Birmingham, USA)

miniKanren is a family of constraint logic programming languages designed for exploring *relational programming*. That is, every program written in miniKanren represents a mathematical relation, and every argument to that program can be a fresh logic variable, a ground term, or a partially ground term containing logic variables. The miniKanren language and implementation has been carefully designed to support this relational style of programming---for example, miniKanren uses a complete, biased, interleaving search by default, and unification always uses the occurs check.

miniKanren provides constraints useful for writing interpreters, type inferencers, and parsers as relations. One interesting class of miniKanren programs are interpreters written for a Turing-complete subset of Lisp, supporting lists, symbols, mutual recursion, and higher-order functions. Since these interpreters are written as relations, they can perform advanced tasks such as example-based program synthesis "for free." By taking advantage of the declarative properties of miniKanren, and the semantics of Lisp, we have been able to speed up some synthesis problems by 9 orders of magnitude with respect to the default miniKanren search. We are actively exploring how to use machine learning and neural networks to further improve synthesis search.

miniKanren has also been used to prototype language semantics, similarly to semantics engineering tools like PLT Redex. One variant of miniKanren---alphaKanren, inspired by alphaProlog---supports nominal unification, and is useful for implementing capture-avoiding substitution. miniKanren's relational nature makes creating an executable semantics for a language easy in some ways, frustrating in others.

The most recent use of miniKanren is as the foundation of mediKanren, a language and system for reasoning over biomedical data sources, as part of the National Institutes of Health's Center For Advancing Translational Sciences (NCATS) Data Translator project. We have scaled miniKanren to reason over SemMedDB, a graph database of 97 million biomedical facts, and are integrating other data sources into the mediKanren system.

Finally, miniKanren is designed to be easy to understand, teach, implement, and hack. Implementing the miniKanren core language (microKanren) has become a standard part of learning miniKanren; as a result, there are hundreds of implementations of miniKanren, embedded in dozens of host languages. We have invested great effort in writing accessible books and papers on miniKanren, giving talks at industry and academic conferences, teaching summer schools and tutorials, etc. One interesting result of these efforts is that we have developed a loose, distributed group of miniKanren researchers around the world.

In my talk I will explore these aspects of miniKanren, describe the lessons we have learned over the past 15 years, and outline the directions for future work.

Can Programming be Liberated from Unidirectional Style?

Zhenjiang Hu (National Institute of Informatics, SOKENDAI, Japan)

Programs usually run unidirectional; computing output from input and output is not changeable. It is, however, becoming more and more important to develop programs whose output is subject to change. One typical example is data synchronization, where we may want to have a consistent schedule information by synchronizing calendars in different formats on various systems, make a smart watch by synchronizing its configuration with the environment, or achieve data interoperability by synchronization data among subsystems. This situation imposes difficulty in using the current unidirectional programming languages to construct such synchronization programs, because it would require us to develop and maintain several unidirectional programs that are tightly coupled and should be kept consistent with each other.

In this talk, I will start by briefly reviewing the current work on bidirectional programming, a new programming paradigm for developing well-behaved bidirectional programs in order to solve various synchronization problems. I will then discuss the essence of bidirectional programming, talk about our recent progress on putback-based bidirectional programming, and show a framework for supporting systematical development of bidirectional programs. Finally, I will highlight its potential application to lay the software foundations for controlling, integrating, and coordinating decentralized data.

Building verified cryptographic components using F*

Cédric Fournet (Microsoft)

The HTTPS ecosystem includes communications protocols such as TLS and QUIC, the X.509 public key infrastructure, and various supporting cryptographic algorithms and constructions. This ecosystem remains surprisingly brittle, with practical attacks and emergency patches many times a year. To improve their security, we are developing high-performance, standards-compliant, formally verified implementation of these components. We aim for our verified components to be drop-in replacements suitable for use in mainstream web browsers, servers, and other popular tools.

In this talk, I will give an overview of our approach and our results so far. I will present our verification toolchain, based on F*: a programming language with dependent types, programmable monadic effects, support for both SMT-based and interactive proofs, and extraction to C and assembly code. I will also illustrate its application using security examples, ranging from the functional correctness of optimized implementations of cryptographic algorithms to the security of (fragments of) the new TLS 1.3 Internet Standard.

See https://fstar-lang.org/ for an online tutorial and research papers on F*, and https://project-everest.github.io/ for its security applications to cryptographic libraries, TLS, and QUIC.

[FLOPS 2018 home]