Day  Week 1  Week 2  

AM 1  AM 2  PM 1  PM 2  AM 1  AM 2  PM 1  PM 2  
MON  
TUE  
WED  
THR  
FRI  
SAT 
Videography by Ken Maupin
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 typesafe Persistent Merkle Tree This talk will demonstrate to the audience how OCaml's advanced functional programming features can be used to make typesafe 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 tracebased 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: Turingcomplete, 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 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. 
8:30PM  Robbert Gurdeep Singh  Multiverse debugging in Voyager: a proof of concept multiverse debugger that takes as input Featherweight AmbientTalk programs written in PLTRedex, 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 
Tagbased 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. Tagbased reference monitors provide a generic mechanism to enforce dynamic policies without rewriting code. In this talk I introduce a monitor model for a Clike 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 typechecks. 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. 