Haskell's type system is expressive and helps catch many errors. However, there is a large number of properties that Haskell's type systems cannot express. This is where dependently typed languages like Agda, Coq, or Idris come into play.
In this Talk, Francesco Mazzoli will give us an overview about what it feels to program in Agda, i.e., he'll provide an outlook on one possible future for high-assurance programming.
We are meeting once a month to share knowledge of and experience with Haskell.
Each time, one of us presents a topic, be it a library, a programming technique, development tools, or internals of GHC or other implementations. The format varies depending on the topic and the presenter between hands-on workshops, discussions and lectures.
Prior knowledge certainly helps, but we definitely don't require you to be an expert to join and/or to present a topic. The only thing that is important is that you are interested in Haskell and that you are eager to learn more.