#### Overview
This seminar is centered around models of programming languages and advanced
reasoning techniques that they can be used to justify. We will study some of
the recent advances in both relational techniques (which can justify
equivalence or refinement of programs) and program logics (which can be used
to establish a formal specification of a program fragment). After covering
some introductory topics, I would like to focus on an in-depth reading of a
small number of research papers that would cover some of the following
subjects:
* reasoning about recursive types,
* reasoning about higher-order state,
* reasoning about shared-memory concurrency,
* separation logic and its models,
* separation logic and concurrency.
The precise scope will be determined together with the participants, taking
into account dependencies in the reading material, and the amount of time
required to understand the material.
#### Literature
The literature could encompass some of the following papers (the list is by no
means exhaustive):
* A. Ahmed, D. Dreyer and A. Rossberg, _State-Dependent Representation Independence._ POPL 2009
* D. Dreyer, A. Ahmed and L. Birkedal, _Logical Step-Indexed Logical Relations._ LICS 2009
* J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang, _Nested Hoare triples and frame rules for higher-order store._ LMCS 7, 2011
* L. Birkedal, F. Sieczkowski, and J. Thamsborg, _A concurrent logical relation._ CSL 2012
* J. C. Reynolds, _Separation Logic: A Logic for Shared Mutable Data Structures._ LICS 2002
* P. W. O'Hearn, _Resources, Concurrency and Local Reasoning._ TCS 2007
* T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang, _Views: Compositional reasoning for concurrency._ POPL 2013
* R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer, _Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning._ POPL 2015
* L. Birkedal, R. Møgelberg, J. Schwinghammer, and K. Støvring, _First steps in synthetic guarded domain theory: step-indexing in the topos of trees._ LMCS 8, 2012
#### Prerequisites
* Logic for Computer Scientists
* Methods of Programming
* Theoretical Foundations of Programming Languages
* Semantics of Programming Languages (recommended)
* Program Verification (recommended)
