Wednesday, June 12  

9:00 
Welcome and refreshment

9:15–9:30 

9:30–10:30
Chair: William J. Bowman 
Stooping to program lowlevel, imperative code is sometimes unavoidable, but specifying and verifying low level code can, thankfully, be significantly more abstract. F* (https://fstarlang.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 monadindexed monads; data manipulation code is typed using lensindexed lenses; zerocopy, imperative parsers and built from a library of parserindexed 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://projecteverest.github.io) which uses F* to build and deploy high performance, verified, secure implementations of cryptographic communication protocols. 
10:30–11:00 
Coffee Break

11:00–11:30
Chair: Matteo Cimini 
Transforming programs into continuationpassing style is a common intermediate form that allows programs to be evaluated using a bounded amount of control context. In essence, the transformation into continuationpassing style makes the control context explicit and eliminates all nontail 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 continuationpassing 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 continuationpassing 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. 
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 errorprone. 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 higherorder 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. 
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. 
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 runtime cost, and other generic combinators for composing quotients. 
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 cofounded 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 ecommerce. Together, these examples give a reasonable overview of the way QuickCheck has been used in industrial practice. 
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. 
11:30–12:00 
Many developers trying propertybased 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 nontrivial—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 sidestep the “where do I start?” question, and quickly derive the benefits that propertybased testing has to offer. 
12:00–12:15 

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 decisionmaking, 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 gradientbased 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. 
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. 
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 CPSbased 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 tracebased approach of PyProb, a followup probabilistic programming system focused on amortized inference with deep learning in Python. Finally we will emphasize the tradeoffs 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. 
15:00–15:30 
Coffee Break

15:30–15:45 
Closing Remarks

Transforming programs into continuationpassing style is a common intermediate form that allows programs to be evaluated using a bounded amount of control context. In essence, the transformation into continuationpassing style makes the control context explicit and eliminates all nontail 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 continuationpassing 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 continuationpassing 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.  
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 runtime cost, and other generic combinators for composing quotients.  
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.  
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 errorprone. 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 higherorder 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.  
Many developers trying propertybased 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 nontrivial—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 sidestep the “where do I start?” question, and quickly derive the benefits that propertybased testing has to offer.  
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.  
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.  
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. 