Oregon Programming Languages Summer School

Types, Logic, Semantics, and Verification

University of Oregon — Eugene OR

June 15-27, 2015


June 15-27, 2015

Types, Logic, Semantics, and Verification

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.

© University of Oregon Department of Computer and Information Science, 1202 University of Oregon, Eugene OR 97403-1202