The program consists of more than twenty-five, 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.

Introduction Matthew Fluett

SMT Solvers - Theory, Implementation and Applications Leonardo de Moura, Microsoft

Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). SMT solvers decide logical satisfiability (or dually, validity) of formulas in classical multi-sorted first-order logic with equality, with respect to a background theory. The success of SMT for verification applications is largely due to the suitability of supported background theories for expressing verification conditions.

These lectures will present the theory behind SMT solvers, and the main implementation techniques used. The speaker will also describe how SMT solvers are used in industry and Microsoft in particular.

Mechanization of Metatheory Using lf and twelf Robert Harper, Carnegie Mellon University

The lectures will discuss the use of Twelf in formalizing programming language metatheory, i.e., describing logically the formal properties of programming languages and reasoning about them with the help of a proof assistant.

Compiler Construction in Formal Logical Frameworks Jason Hickey, California Institute of Technology

In recent years, there have been many advances in formal compiler construction. Formal compilers are highly declarative, which has several benefits. Formal compilers can be verified; their logical construction is often much simpler than traditional methods; and compiler implementations are very close to textbook specifications. A potential disadvantage is that non-local code analysis can sometimes be difficult to formalize. In this course, we’ll look at the tools, methods, and models being used for formal compiler development. In addition, we’ll cover many compiler phases, comparing the formal definition with traditional ad-hoc techniques.

Specification and Verification of Programs with Pointers Rustan Leino, Microsoft

The lectures will cover techniques on verifying complex programs using a mixture of two source languages: the object-oriented language Spec#, which includes a verification methodology that defines usage rules, and the object-based language Dafny, which uses the idioms of dynamic frames for specifying behavior. Both languages translate into the Boogie language and are then verified using the Boogie program verifier.

Particular emphasis will be paid to the complexities of verifying programs with pointers, using appropriate memory models that capture the high-level uses of common programming languages while enabling good tool support.

Leveraging Domain-Specific Languages for Reasoning Sorin Lerner, University of California – San Diego

A Domain-Specific Language (DSL) is a language designed for expressing programs in a particular domain. For example, one can have a special language for writing sensor-network software, a language for expressing security policies, or a language for expressing computations that use a specialized programming paradigms like map-reduce. By providing the right abstractions for a particular domain, a DSL makes it easier for humans to write, maintain and extend software, thus reducing the potential for errors. More importantly, however, the restricted domain of a DSL allows automated tools to take advantage of the DSL’s stylized form in order to achieve automated reasoning abilities that would be impossible otherwise.

These lectures will explore ideas and topics related to using a DSL for achieving better logical reasoning abilities. It will first describe a concrete example of using a DSL in this way, namely the Rhodium language for expressing compiler optimizations, and the associated tool for automatically proving these optimizations' correctness. Using this example as a starting point, and the lessons learned from the Rhodium project, the talk will explore some of the vast design space of DSLs and the associated tradeoffs in terms of expressiveness of the language, automation of the logical reasoning abilities, and efficiency of the execution engine.

Reasoning About Programs with ACL2 Pete Manolios, Northeastern University

ACL2, A Computational Logic for Applicative Common Lisp, is a pure functional programming language, a first-order logic, and an automated theorem prover. ACL2 has been used to prove some of the most complicated theorems ever proved about commercial systems.

These lectures will study the logical foundations of ACL2. The speaker will discuss termination analysis in depth, since it plays a key role in ACL2. For example, all defined functions have to be proven to terminate, and termination analysis is used to justify induction schemes. The speaker will present several applications of ACL2 and give a demo using the ACL2 Sedan, a version of ACL2 that is being used to teach freshman students how to reason about programs.

Putting the Curry-Howard Isomorphism to Work Tim Sheard, Portland State University

There has been a lot of recent interest in exploiting the Curry- Howard isomorphism in type systems for more or less traditional programming languages. Types based upon the Curry-Howard isomorphism can express precise properties of programs. The speaker will discuss the Omega system in which the specification of designs, the definition of properties, the implementation of programs, and the checking that programs adhere to their properties, are all bundled in a coherent manner into a single unified system that appears to the user to be a programming language.

At the summer school, the speaker will introduce the basic ideas from scratch, and give many, many examples that illustrate its use. The talk is not addressed at experts in type systems, but to general computer scientists who are interested in describing properties of their progams precisely. Participants will be taught to use Omega as a broad spectrum language, capable of handling abstract properties as well as implementation minutiae, where the connection between properties and programs is formal and precise.

Nominal Techniques Christian Urban, TU Munich

Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs about programming languages, especially in proofs by induction. Nominal techniques are about having names as binders and providing an infrastructure to reason conveniently about them. In the course, the speaker will give an overview about the nominal techniques as they are implemented in the theorem prover Isabelle/HOL.

Specific topics include Permutations and the notion of support; Strong induction principles that have the variable convention already built in; Definition of function by structural recursion over alpha-equivalence classes; Proofs and techniques from structural operational semantics.

Coq for Programming Language Metatheory Stephanie Weirich and Brian Aydemir, University of Pennsylvania

The speakers will present a hands-on tutorial on the use of the Coq proof assistant in formalizing programming language metatheory. The tutorial is tailored to people who are familiar with syntactic proofs of programming language metatheory, such as type soundness, but have never used a proof assistant to create and check such proofs. At the end, participants will have a reading knowledge of Coq and a running start on using Coq in their own work. The tutorial is composed of two pieces: a basic introduction to defining language semantics in Coq as well as the proof of simple results, as well as a more specialized treatment of the representation of binding structures. Both parts include interactive demos and exercises.

This tutorial material was developed in collaboration with Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic, all members of the Penn PLCLUB.