University of Oregon University of Oregon

Foundations of Probabilistic Programming and Security

June 17-29, 2019

Day Week 1 Week 2
AM 1 AM 2 PM 1 PM 2 AM 1 AM 2 PM 1 PM 2
MON Pfenning Silva Pfenning Silva     Ahmed Gordon Ahmed
TUE Myers Pfenning Myers Henglein Ahmed Gordon Leino
WED Pfenning Harper Myers Silva Ahmed Swamy Henglein Gordon
THR Myers Harper Hoffmann Silva Henglein Staton Swamy Henglein
FRI Hoffmann Harper Hoffmann Staton Swamy Staton
SAT Hoffmann Harper Swamy Staton

Videography by Ken Maupin

Amal Ahmed — Northeastern University

Secure Compilation

Survey paper on Formal Approaches to Secure Compilation

Online Appendix with additional survey of proof techniques

The Next 700 Compiler Correctness Theorems (Functional Pearl). Daniel Patterson and Amal Ahmed, ICFP 2019.

Lecture 1, Slides | Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4 | Lecture 2, Notes

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Slides

Andrew Gordon — Microsoft Research

Empowering Spreadsheet Users with Probabilistic Programming

Summary Paper: Probabilistic_Programming_for_End_Users

Lecture 1, Slides | Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

Lecture 2, Slides | Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Lecture 3, Slides | Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Robert Harper — Carnegie Melon University

Practical Foundations for Programming Languages

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4 | Lecture 1, Notes

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Video Part 4 | Lecture 4, Notes | Lecture 4, Notes

Fritz HengleinDeon Digital AG and University of Copenhagen

Smart Declarative Contracts

Lecture 1, Lecture Slides | Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3

Lecture 2, Lecture Slides | Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Lecture 4, Lecture Slides | Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Jan Hoffmann — Carnegie Melon University

Resource Analysis

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Notes

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4 | Lecture 2, Notes

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4 | Lecture 3, Notes

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Notes

Rustan Leino — Amazon

Writing Verified Software for Production

Lecture Slides

Andrew Myers — Cornell University

Security-Typed Languages

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4 | Lecture 1, Notes

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Notes

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4 | Lecture 3, Notes

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Notes

Frank Pfenning — Carnegie Melon University

Session-Typed Concurrent Programming

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4 | Lecture 1, Video Part 5 | Lecture 1, Video Part 6 | Lecture 1, Notes

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4 | Lecture 2, Notes

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4 | Lecture 3, Notes

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Video Part 4

Bonus Lecture, Video Part 1 | Bonus Lecture, Video Part 2 | Bonus Lecture, Video Part 3

Alexandra Silva — University College London

Coalgebraic Semantics

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4 | Lecture 1, Video Part 5 | Lecture 1, Video Part 6 | Lecture 1, Notes

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4 | Lecture 2, Notes

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Notes

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Video Part 4 | Lecture 4, Notes

Sam Staton — University of Oxford

Probabilistic programming: Bayesian Non-Parametrics and Semantics

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4
Sample Haskell Code
To compile and run the sample, type
stack build
stack run
this may take awhile.

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Nikhil Swamy — Microsoft Research

Verifying Low-level Code for Security and Correctness Properties using F*

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Participant Talks

Day Time Presentor Title
TUE 8:00PM Breandan Considine Kotlin∇: A Shape Safe eDSL for Differentiable Functional Programming
How does automatic differentiation work? What makes a program differentiable? Come to this talk to learn more!
8:30PM Paul He Interaction Trees: Representing Recursive and Impure Programs in Coq I'll talk about a framework in Coq for formalizing the behavior of possibly nonterminating programs that also interact with the external world.
THR 8:00PM John Wu Designing More Secure Cryptographic Primitives: A type-safe Persistent Merkle Tree
This talk will demonstrate to the audience how OCaml's advanced functional programming features can be used to make type-safe cryptograph data structures.
8:30PM Will Crichton Modeling Spatiotemporal Concepts with Probabilistic Programs
How can we elevate the role of humans in computer vision beyond data labelers or hyperparameter tuners? This talk explores a speculative future where probabilistic programming lies at the interface between data scientists and machine learning models by expressing domain knowledge and structural relationships.
9:00PM Ana McTaggart Privacy Protecting Information Flow
This talk will cover oblivious information flow, and my work on how to obfuscate access patterns by treating accesses as information flow. By obfuscating these access patterns, we obfuscate metadata, which otherwise reveals significant information about the data transmitted.
9:30PM Carmine Abate Different observations for correct and secure compilation
We revisit some trace-based criteria for correct and secure compilation in a scenario in which target observations can be significantly different from source ones.
MON 8:00PM Christian Weilbach Anglican Tutorial: Turing-complete, functional Probabilistic Programming as a Domain Specific Language
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.
8:30PM Robbert Gurdeep Singh Multiverse debugging in Voyager: a proof of concept multiverse debugger that takes as input Featherweight AmbientTalk programs written in PLT-Redex, and allows programmers to interactively browse all possible execution states by means of multiverse breakpoints and stepping commands.
9:00PM Zhe Zhou Sometime, people want to do some complex work on machines with time and space limitation, with a tolerance of losing accuracy. Approximation is a good way to resolve it. Of course, approximated programs are quite different from the original programs, people have to modify them. Is it possible to use a compiler or a program synthesizer to convert a normal program to approximated program? I am wondering to use a monadic perspective to think about this problem.
9:30PM Sean Anderson Tag-based Micropolicies for C
We've seen instances of specific Information Flow Control and related policies implemented via types and specialized hardware. Now let's get general. Tag-based reference monitors provide a generic mechanism to enforce dynamic policies without rewriting code. In this talk I introduce a monitor model for a C-like language and discuss some of the policies it can implement.
WED 8:00PM Mikkel Kragh Mathiesen Advanced (co)discrimination for efficient (co)partitioning and (co)sorting: Discrimination is a technique for efficient partitioning and sorting with respect to a wide range of equivalence relations and orders, using a synthetic theory of relations. We show how to deal with the usual orders on rational numbers, algebraic numbers and even real numbers. To this end the synthetic theory needs to be extended and we introduce the notion of codiscrimination as a technique for copartitioning and cosorting. Finally, we show that any decidable order relation can be encoded using these techniques.
8:30PM Noric Couderc Apple is the default fruit
The point of a software library is to provide a number of tools for solving a problem or a set of related problems. Many of these tools serve a similar purpose, but have different properties regarding performance. Therefore, software developers are often faced with a set of equivalent tools to solve a problem and this equivalence is reflected in the type system, but picking the wrong tool might lead to significant changes in the behaviour of the program, even though it type-checks. This talk will be an attempt at exposing various aspects of the issue, as well as several potential solutions.
9:00PM Kiran Gopinathan Formal Analysis of Probabilistic Algorithms
How can we capture the notion of a probability distribution within constructive logics? How can these structures be used to verify properties of probabilistic programs? This talk provides an overview of the current approaches for reasoning about probability within Coq, discussing how these concepts translate when reasoning about probabilistic programs. These will also be contextualised within an ongoing project on verifying the probabilistic properties of distributed systems.