This is an advanced programming language seminar on recent advances in
programming languages including extensible effects, type theory, dependent
types, Agda, homotopy type theory.

One of the main goals is to gain the necessary background to appreciate
recent papers such as:

From ICFP 2013:

  Programming and Reasoning with Algebraic Effects and Dependent Types
  Edwin Brady

  Handlers in Action
  Ohad Kammar, Sam Lindley and Nicolas Oury

  Towards Dependently Typed Haskell: System FC with Kind Equality
  Stephanie Weirich, Justin Hsu and Richard A. Eisenberg

From Haskell Symposium 2013:

  Oleg Kiselyov, Amr Sabry and Cameron Swords. Extensible Effects: An
  Alternative to Monad Transformers

  Sam Lindley and Conor McBride. Hasochism: The Pleasure and Pain of
  Dependently Typed Haskell Programming

And the recent published book on homotopy type theory:

  http://homotopytypetheory.org/book/

There will likely be several Haskell and Agda programming exercises to
consolidate the concepts and experiment with new ideas.