TFP 2019 Program

Program

Click a title to see the abstract. The speaker is emphasized in the author list.
Wednesday, June 12
9:00
Welcome and refreshment
9:15–9:30

Ron Garcia
9:30–10:30
Chair: William J. Bowman

Stooping to program low-level, imperative code is sometimes unavoidable, but specifying and verifying low level code can, thankfully, be significantly more abstract.

F* (https://fstar-lang.org) is a programming language and proof assistant that enables the construction of verified C and assembly programs using dependent type theory.

At the core of F*'s verification methodology is to specify programs using indexed types, where the indexes capture correctness properties of programs using classic functional programming patterns "one level up". For instance, effectful computations in F* are, broadly, described using monad-indexed monads; data manipulation code is typed using lens-indexed lenses; zero-copy, imperative parsers and built from a library of parser-indexed parser combinators; and so on.

In this talk, I'll give a taste of F* programming through a series of examples, drawing on experience from Project Everest (https://project-everest.github.io) which uses F* to build and deploy high performance, verified, secure implementations of cryptographic communication protocols.

Nikhil Swamy
10:30–11:00
Coffee Break
11:00–11:30
Chair: Matteo Cimini

Transforming programs into continuation-passing style is a common intermediate form that allows programs to be evaluated using a bounded amount of control context. In essence, the transformation into continuation-passing style makes the control context explicit and eliminates all non-tail function calls. The explicit control context is traditionally thought of as a function, known as a continuation, that knows how to finish the computation. Although this abstraction is attractive, naive implementations can suffer from excessive closure allocations for continuations. In fact, an impressive amount of work has been done to reduce closure allocation for programs in continuation-passing style with varying degrees of success. This article describes a newly undertaken project to explore novel implementation strategies for closureless CPS. That is, this article presents a CPS transformation that eliminates the need to dynamically allocate continuation closures by storing on a stack the information that a traditional continuation would require. There are, of course, several design choices that need to be made to represent a program in closureless continuation-passing style. This article outlines the different representations that our new project proposes to empirically study. In addition, the articles outlines the potential advantages and disadvantages of each proposed representation.

Marco T. Morazan, Shamil Dzhatdoyev, Josephine Des Rosiers
11:30–12:00

A selective CPS transformation enables us to execute a program with delimited control operators, shift and reset, in a standard functional language without support for control operators. The selective CPS transformation dispatches not only on the structure of the input term but also its purity: it transforms only those parts that actually involve control effects. As such, the selective CPS transformation consists of many rules, each for one possible combination of the purity of subterms, making its verification tedious and error-prone. In this paper, we first formalize (a monomorphic version of) the selective CPS transformation in the Agda proof assistant. We use intrinsically typed term and context representations together with parameterized higher-order abstract syntax (PHOAS) to represent binding structures. We then prove the correctness of the transformation, i.e., the equality of terms is preserved by the CPS transformation. Thanks to the formalization, we confirmed that all the rules of the selective CPS transformation in the previous work are correct, but found that one lemma on the behavior of shift was not precise.

Chiaki Ishio, Kenichi Asai
12:00–14:00
Lunch
14:00–14:30
Chair: John Hughes

We present a translation that converts a set constraint formula into an SMT problem. Our technique allows for arbitrary boolean combinations of positive or negative set constraints,and leverages the performance of modern solvers such as Z3. To show the usefulness of unrestricted set constraints,we use them to devise a pattern match analysis for functional languages. This analysis ensures that missing cases of pattern matches are always unreachable. We implement our analysis in the Elm compiler and show that the our translation is fast enough to be used in practical verification.

Joseph Eremondi
14:30–15:00

Reasoning about programs and their values is a common motivation for a dependently typed programming language. However, sometimes the privileged equality of the language is not the desired equality of the programmer. Quotient types are a solution to this problem where, for the values of the quotient type, the privileged equality of the language is equivalent to a desired equivalence relation. We demonstrate an efficient encoding of quotient types defined by normalization in Cedille, a new dependently typed programming language, with concrete examples and a generic type. Moreover, we formalize two variants of generic function lifting, one of which is zero run-time cost, and other generic combinators for composing quotients.

Andrew Marmaduke, Christopher Jenkins, Aaron Stump
15:00–15:30
Coffee Break
Thursday, June 13
9:00
Welcome and refreshment
9:30–10:30
Chair: Ron Garcia

QuickCheck is a random testing tool that Koen Claessen and I invented, which has since become the testing tool of choice in the Haskell community. In 2006 I co-founded Quviq, to develop and market an Erlang version, which we have since applied for a wide variety of customers, encountering many fascinating testing problems as a result. This talk introduces Quviq QuickCheck, and in particular the extensions made for testing stateful code, via a toy example in C. It goes on to describe the largest QuickCheck project to date, which developed acceptance tests for AUTOSAR C code on behalf of Volvo Cars. Finally it explains a race detection method that nailed a notorious bug plaguing Klarna, northern Europe's market leader in invoicing systems for e-commerce. Together, these examples give a reasonable overview of the way QuickCheck has been used in industrial practice.

John Hughes
10:30–11:00
Coffee Break
11:00–11:30
Chair: Marco Morazan

In this paper we set forth the thesis that a language type checker can be an effective tool in teaching language design principles of functional languages. We have used TypeSoundnessCertifier, a tool for type checking languages and certifying their soundness, in the context of a graduate course in programming languages. In this paper, we offer details on how the course took place, and we report on some data gathered during evaluations. Although the work reported in this paper is not statistically significant, we share our experience to show the type of studies that we are conducting, and to inspire similar and larger studies towards gathering evidence for, or against, our thesis.

Matteo Cimini
11:30–12:00

Many developers trying property-based testing for the first time find it difficult to identify properties to write—and find the simple examples in tutorials difficult to generalize. This is known as the oracle problem, and it is common to all approaches to testing that use test case generation. In this paper, therefore, we take a simple—but non-trivial—example of a purely functional data structure, and present five different approaches to writing properties, along with the pitfalls of each to keep in mind. We compare and constrast their effectiveness with the help of eight buggy implementations. We hope that the concrete advice presented here will enable readers to side-step the “where do I start?” question, and quickly derive the benefits that property-based testing has to offer.

John Hughes
12:00–12:15

John Hughes
12:00–14:00
Lunch
14:00–15:00
Nitobe Gardens.
We'll walk from TFP at 2:00.
15:00–16:00
Museum of Anthropology
We'll walk from Nitobe at about 15:00.
17:30
Enigma Cafe on 10th Ave.
A group will take the 99 or 14 from UBC at 17:00. It's a 55 minute walk from MOA for those who want to walk.
Friday, June 14
9:00
Welcome and refreshment
9:30–10:30
Chair: Ron Garcia

Probabilistic programming uses programming language techniques to make it easy to denote and perform inference in the kinds of probabilistic models that inform decision-making, accelerate scientific discovery, and underlie modern attacks on the problem of artificial intelligence. Deep learning uses programming language techniques to automate supervised learning of program parameter values by gradient-based optimization. What happens if we put them together? This talk will review probabilistic programming. It will also introduce inference compilation and address how linking deep learning and probabilistic programming is leading to powerful new AI techniques while also opening up significant new research questions.

Frank Wood
10:30–11:00
Coffee Break
11:00–11:30
Chair: William J. Bowman

In this paper we extend a rank 2 intersection type system with gradual types. We then show that the problem of finding a principal typing for a lambda term, in a rank 2 gradual intersection type system is decidable. We present a type inference algorithm which builds the principal typing of a term through the generation of type constraints which are solved by a new extended unification algorithm constructing the most general unifier for rank 2 gradual intersection types.

Pedro Ângelo, Mário Florido
11:30–12:00
Cancelled due to unforeseeable events
12:00–14:00
Lunch
14:00–15:00
Chair: William J. Bowman

Anglican is a powerful probabilistic programming system that is embedded as a DSL in the functional programming language Clojure. Introduced in 2014, it established a CPS-based compiler for a Turing complete subset of Clojure and pioneered a diverse set of concepts in the probabilistic programming community such as integration with Bayesian Optimization or amortized inference. It exploits Clojure's persistent data structures to provide a minimal,functional interface to inference algorithms. This talk both introduces Anglican with examples and describes how such a system can be implemented in a few hundred lines of code. The talk will also contrast it with the trace-based approach of PyProb, a follow-up probabilistic programming system focused on amortized inference with deep learning in Python. Finally we will emphasize the trade-offs and challenges between functional environments and the popular Python environment as design objectives for a new functional, probabilistic programming language for numerical and statistical programming.

Christian Weilbach
15:00–15:30
Coffee Break
15:30–15:45
Closing Remarks

Accepted Talks

Transforming programs into continuation-passing style is a common intermediate form that allows programs to be evaluated using a bounded amount of control context. In essence, the transformation into continuation-passing style makes the control context explicit and eliminates all non-tail function calls. The explicit control context is traditionally thought of as a function, known as a continuation, that knows how to finish the computation. Although this abstraction is attractive, naive implementations can suffer from excessive closure allocations for continuations. In fact, an impressive amount of work has been done to reduce closure allocation for programs in continuation-passing style with varying degrees of success. This article describes a newly undertaken project to explore novel implementation strategies for closureless CPS. That is, this article presents a CPS transformation that eliminates the need to dynamically allocate continuation closures by storing on a stack the information that a traditional continuation would require. There are, of course, several design choices that need to be made to represent a program in closureless continuation-passing style. This article outlines the different representations that our new project proposes to empirically study. In addition, the articles outlines the potential advantages and disadvantages of each proposed representation.

Marco T. Morazan, Shamil Dzhatdoyev, Josephine Des Rosiers

Reasoning about programs and their values is a common motivation for a dependently typed programming language. However, sometimes the privileged equality of the language is not the desired equality of the programmer. Quotient types are a solution to this problem where, for the values of the quotient type, the privileged equality of the language is equivalent to a desired equivalence relation. We demonstrate an efficient encoding of quotient types defined by normalization in Cedille, a new dependently typed programming language, with concrete examples and a generic type. Moreover, we formalize two variants of generic function lifting, one of which is zero run-time cost, and other generic combinators for composing quotients.

Andrew Marmaduke, Christopher Jenkins, Aaron Stump

In this paper we set forth the thesis that a language type checker can be an effective tool in teaching language design principles of functional languages. We have used TypeSoundnessCertifier, a tool for type checking languages and certifying their soundness, in the context of a graduate course in programming languages. In this paper, we offer details on how the course took place, and we report on some data gathered during evaluations. Although the work reported in this paper is not statistically significant, we share our experience to show the type of studies that we are conducting, and to inspire similar and larger studies towards gathering evidence for, or against, our thesis.

Matteo Cimini

A selective CPS transformation enables us to execute a program with delimited control operators, shift and reset, in a standard functional language without support for control operators. The selective CPS transformation dispatches not only on the structure of the input term but also its purity: it transforms only those parts that actually involve control effects. As such, the selective CPS transformation consists of many rules, each for one possible combination of the purity of subterms, making its verification tedious and error-prone. In this paper, we first formalize (a monomorphic version of) the selective CPS transformation in the Agda proof assistant. We use intrinsically typed term and context representations together with parameterized higher-order abstract syntax (PHOAS) to represent binding structures. We then prove the correctness of the transformation, i.e., the equality of terms is preserved by the CPS transformation. Thanks to the formalization, we confirmed that all the rules of the selective CPS transformation in the previous work are correct, but found that one lemma on the behavior of shift was not precise.

Chiaki Ishio, Kenichi Asai

Many developers trying property-based testing for the first time find it difficult to identify properties to write—and find the simple examples in tutorials difficult to generalize. This is known as the oracle problem, and it is common to all approaches to testing that use test case generation. In this paper, therefore, we take a simple—but non-trivial—example of a purely functional data structure, and present five different approaches to writing properties, along with the pitfalls of each to keep in mind. We compare and constrast their effectiveness with the help of eight buggy implementations. We hope that the concrete advice presented here will enable readers to side-step the “where do I start?” question, and quickly derive the benefits that property-based testing has to offer.

John Hughes

In this paper we extend a rank 2 intersection type system with gradual types. We then show that the problem of finding a principal typing for a lambda term, in a rank 2 gradual intersection type system is decidable. We present a type inference algorithm which builds the principal typing of a term through the generation of type constraints which are solved by a new extended unification algorithm constructing the most general unifier for rank 2 gradual intersection types.

Pedro Ângelo, Mário Florido

We present a translation that converts a set constraint formula into an SMT problem. Our technique allows for arbitrary boolean combinations of positive or negative set constraints,and leverages the performance of modern solvers such as Z3. To show the usefulness of unrestricted set constraints,we use them to devise a pattern match analysis for functional languages. This analysis ensures that missing cases of pattern matches are always unreachable. We implement our analysis in the Elm compiler and show that the our translation is fast enough to be used in practical verification.

Joseph Eremondi

Interactive web applications need to handle the communication between server and client web browsers. In the iTasks system, this is delegated to a general purpose component, called editor. Editors allow fine grained control over the point of execution on the server, using native code, which is efficient, and on the client, using JavaScript, which is much less efficient. One particular use case of editors uses the W3C Scalable Vector Graphics standard to allow applications to fully customize the look and feel of an editor, called SVG editor. The current implementation is operational, but there is room for improvement, both in terms of code structure and performance. We show how to improve the code structure of SVG editors and at the same time increase their performance. Both improvements are obtained by separating the logic into two embeddings: first, a deep embedding to obtain an isomorphic representation of the image code, and second, a shallow embedding to calculate the actual SVG rendering and proper layout of the deep representation of the image.

Peter Achten, Rinus Plasmeijer