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.