Nada Amin — CLP(SMT)
We show how easy it is to hook an SMT (Satisfiability Modulo Theory) solver such as CVC4 or Z3 as a backend to miniKanren, an embedded domain-specific language in Scheme, to create an environment for constraint logic programming. We describe the simple implementation and illustrate the technology through interpreters, synthesis, and symbolic execution.
Link to websiteNate Foster — p4v or: How I Learned to Stop Worrying and Trust Z3
We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes.
Download slidesDownload paper
Nate Foster — Probabilistic NetKAT
We develop new techniques for reasoning about probabilistic network programs. The core of our approach is based on a semantic characterization of the history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. The key technical challenge lies in computing the semantics of the iteration operator, which we handle using an encoding in the style of a small-step operational semantics. We present a prototype implementation and develop heuristic optimizations that enable it to scale to networks of realistic size. Using examples, we show how our method can be used to establish generic properties such as program equivalence and refinement, as well as program-specific properties such as resilience to failures. We compare the scalability of our implementation against a state-of-the art tool, and we develop an extended case study involving a recently proposed design for data center networks.
Download slidesDownload paper
Link to website
Ron Garcia — Improving Abstract Gradual Typing Semantics
Abstracting Gradual Typing (AGT) is an approach to systematically constructing gradually-typed languages from statically-typed ones. Their semantics satisfy a number of desirable properties, including type safety, and criteria for gradual typing. However, the resulting semantics saturate programs with runtime checks, no matter how static the program. Hand-crafted gradual languages sparsely populate programs with checks, reducing the number as a program gets more static, culminating in statically-typed programs having no checks. In this talk, we show how to systematically transform AGT semantics to support sparse checking.
Download slidesRobert Harper — Computational Cartesian Cubical Type Theory
We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.
Link to websiteAndrew Kennedy — Typing with Continuations for the Hack Programming Language
In this talk I describe how we formalized the flow-sensitive type system of the Hack programming language, Facebook's replacement for PHP. We use continuation typings to deal with control flow constructs such as conditionals, break, continue, and finally.
Download slidesJohn Reppy — Continuations, threads, and LLVM
This talk describes some ongoing work on the design of compiler intermediate-representations that can support concurrency and parallelism.
Download slidesGabriel Scherer — Keep (re)playing until your get all the successes
In this talk I will show an implementation of angelic non-determinism (as with the `amb` operator) that uses only mutable state and exceptions -- we have pure OCaml and SML implementations, without changingthe compiler or the runtime system. This approach, which relies on a neat trick found by James Koppel, can be extended to an implementation of full delimited continuations! (This is joint work with Jimmy Koppel and Armando Solar-Lezama)
Download slidesGabriel Scherer — Short course on classical realizability
This talk was a blackboard intro course on classical realizability (a realizability interpretation of abstract machines designed to easily be extended to realize computational effects, starting with classic control effects). I introduced positive and negative interpretations of each type of the simply-typed lambda-calculus, sketched a proof of the fundamental lemma -- well-typed terms realize the interpretation of their types -- with weak normalization as a corollary.
Alexandra Silva — Almost Sure Productivity
We define Almost Sure Productivity (ASP), a probabilistic generalization of the productivity condition for coinductively defined structures. Intuitively, a probabilistic coinductive stream or tree is ASP if it produces infinitely many outputs with probability 1. Formally, we define almost sure productivity using a final coalgebra semantics of programs inspired from Kerstan and Koenig. Then, we introduce a core language for probabilistic streams and trees, and provide two approaches to verify ASP: a sufficient syntactic criterion, and a reduction to model-checking pCTL* formulas on probabilistic pushdown automata. The reduction shows that ASP is decidable for our core language. Joint work with Alejandro Aguirre, Gilles Barthe, and Justin Hsu.
Download slidesLink to website
Philip Wadler — Programming Language Foundations in Agda
The leading textbook for formal methods is Software Foundations (SF), written by Benjamin Pierce in collaboration with others, and based on Coq. After five years using SF in the classroom, I have come to the conclusion that Coq is not the best vehicle for this purpose, as too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning programming language theory. Accordingly, I have written a new textbook, Programming Language Foundations in Agda (PLFA). PLFA covers much of the same ground as SF, although it is not a slavish imitation. What did I learn from writing PLFA? First, that it is possible. One might expect that without proof tactics that the proofs become too long, but in fact proofs in PLFAare about the same length as those in SF. Proofs in Coq require an interactive environment to be understood, while proofs in Agda can be read on the page. Second, that constructive proofs of preservation and progress give immediate rise to a prototype evaluator. This fact is obvious in retrospect but it is not exploited in SF (which instead provides a separate normalise tactic) nor can I find it in the literature. Third, that using raw terms with a separate typing relation is far less perspicuous than using inherently-typed terms. SF uses the former presentation, while PLFA presents both; the former uses about 1.6 as many lines of Agda code as the latter, roughly the golden ratio. The textbook is written as a literate Agda script, and can be found here: http://plfa.inf.ed.ac.uk
Download paperLink to website
Stephanie Weirich — "Verifying" the Glasgow Haskell Compiler Core language
This is a work-in-progress talk about using Coq to reason about the implementation of Haskell programs (GHC in particular).
Download slidesSteve Zdancewic — Interaction Trees in Coq
In this talk, I'll describe "Interaction Trees," a datatype that is suited for representing effectful computations in Coq. Interaction trees are coinductively defined (and hence potentially infinite) trees, with nodes that describe the effects of exchanging information with the external environment. The trees are parameterized by a signature of such effects, which provide flexibility and allow for sharing of metatheory across instantiations. Interaction trees are a variant of Kiselyov & Ishii's _freer_ monad. We have found them to be useful in several system developments associated with the DeepSpec project. I'll sketch some of those, focusing on their use in the Verified LLVM semantics, where we're using interaction trees to model interactions with the memory system.
Download slidesLink to website