| 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 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. |