Lecture Schedule
The program consists of a series of 35 lectures and 11 hands-on sessions. The sessions are non-overlapping, so participants will have the opportunity to attend all lectures. Each lecture is 80 minutes, including time for questions.
| Morning | Afternoon | ||||
|---|---|---|---|---|---|
| Date | Session 1 | Session 2 | Session 1 | Session 2 | |
| MON 6/15 | Pfenning | Harper | Morehouse | Hands-On Session | |
| TUE 6/16 | Pfenning | Morehouse | Harper | Hands-On Session | |
| WED 6/17 | Pfenning | Morehouse | Harper | Hands-On Session | |
| THR 6/18 | Pfenning | Morehouse | Harper | Hands-On Session | |
| FRI 6/19 | Pfenning | Morehouse | Harper | Hands-On Session | |
| SAT 6/20 | Dybjer | Chlipala | Dybjer | Hands-On Session | |
| SUN 6/21 | Excursion | ||||
| MON 6/22 | Chlipala | Dybjer | Ahmed | Hands-On Session | |
| TUE 6/23 | Dybjer | Chlipala | Ahmed | Hands-On Session | |
| WED 6/24 | Dybjer | Chlipala | Ahmed | Hands-On Session | |
| THR 6/25 | Chlipala | Ahmed | Bickford | Hands-On Session | |
| FRI 6/26 | Ahmed | Constable | Chlipala | Hands-On Session | |
| SAT 6/27 | Bickford | Constable | |||
Lectures are held in 110 Knight Law Center. Morning sessions begin at 9:00 AM and run until noon. Afternoon sessions begin at 2:00 PM and run until 5:00 PM.
Participant Talks
Participants are encouraged to share their current research. Student talks should be organized as a 10 minute presentation, followed by 10 minutes of question and answer. The point of Participant Talks is to create interest around your research. Talks about unfinished research or future directions are encouraged.
| Date | Time | Presentor | Abstract |
|---|---|---|---|
| TUE 6/16 | 8:00PM | Rodolphe Lepigre | I will present a lightweight framework for generating (extensible) parsers. The system relies on an intuitive BNF-like syntax translated to OCaml expressions using DeCaP: our monadic parser combinator library. |
| 8:20PM | Andrew Ruef | We can use empirical and theoretical techniques from science and programming languages to understand and extend computer security. I'll present some case studies from the last fifteen years of computer security showing where we've been, what we've done and where we could go. | |
| 8:40PM | John Bodeen | The main objective of gratr is summarily so: the generation of linear-time parsers for any unambiguous context free grammars. Ambiguity of CFG's, however is undecidable. This talk will elaborate on the criterion for identifying ambiguity, and show how we can guarantee linear time if the grammar passes our (complete) ambiguity tester. In addition, I will compare our methods to the alternative class of formal analytic grammars known as Parsing Expression Grammars (Bryan Ford 2004), which share the similar design goal of unambiguity. | |
| 9:00PM | Praveen Narayanan | I will motivate the need to support equational reasoning on probabilistic programs | |
| THR 6/18 | 8:00PM | Ted Cooper | Monadic RP — a Haskell implementation of relativistic programming that uses RCU primitives to enforce causal ordering |
| 8:20PM | Rob Blanco | Certification of proof outlines | |
| 8:40PM | Sylvia Grewe | I will present our current prototype of Veritas, a workbench that shall simplify the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. I will focus on the verification part of Veritas, which combines off-the-shelf automated first-order theorem provers with automated proof strategies specific to type systems. | |
| 9:00PM | Ben MacAdam | Differential Restriction Categories | |
| TUE 6/23 | 8:00PM | Alice Pavaux | Linear Logic can be viewed through the Curry-Howard correspondence, giving a computational account to proofs. I will talk about an untyped version of this, called Ludics, where the formulas are dropped to keep only the dynamic aspect of LL proofs. |
| 8:20PM | Michael Coblenz | Programming languages are user interfaces for people to use to write software. As a result, when designing programming languages that are intended to be used by people, one must consider the usability implications of design choices. I'll talk about some approaches to programming language usability research and their limitations. | |
| 8:40PM | Luc Pellissier | The Linear λ-calculus is a very rudimentary calculus, where every argument must be used exactly once, thus allowing only finite computations. Infinitary λ-calculus allows to recover the lost expressivity by incorporating infinite terms in the syntax. We show that the infinitary λ-calculus can be recovered from the linear λ-calculus through a completely canonical and abstract way, derived from the Melliès-Tabareau-Tasson construction for the free exponential in Linear Logic. This line of work tries to shed a light on the everlasting conflict of juxtaposition and glueing that is at the heart of the treatment of infinity in logic. | |
| 9:00PM | Julia Belyakova | ||
| THR 6/25 | 8:00PM | Niccolò Veltri | The delay datatype is used in type theory for modeling non-terminating computations. Two elements of this type are weakly bisimilar intuitively if they either converge to the same value or diverge. The delay datatype is a strong monad. However extending type theory with quotient types à la Hofmann it is impossible to construct a monad structure on top of the delay datatype quotiented by weak bisimilarity. In this talk I will give an overview of the problem and some possible solutions. |
| 8:20PM | Karen Sargsyan | Software Verification for Bioinformatics | |
| 8:30PM | Justin Pombrio | I present preliminary work on a binding specification language dubbed "scope partial orders", and an implementation of it in Haskell where unhygienic transformations over terms are ill-typed. | |
| 9:00PM | Gian Pietro Farina | I will talk about Differential Privacy in Probabilistic Programming, and how this could be useful in Bayesian settings, for instance some areas of machine learning. In particular I'll talk about a functional probabilistic programming language whose type system captures bayesian differentially private computations. |
Talks are held in 220 Deschutes, the Computer Science Colloquim room, beginning at 8PM. The building is locked at night, so please be prompt or you will not be able to enter the building. To schedule a talk, email Jim.