An introdution to Agda by Francesco Mazzoli

  • February 27, 2014 · 7:00 PM

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.

Join or login to comment.

  • Alvaro V.

    Great intro, and finally met Francesco, with whom I had indirectly worked with before.

    February 28, 2014

  • Gerolf S.

    Thanks for this great intro session, Francesco!

    February 28, 2014

  • Bas van D.

    Unfortunately I've to catch a flight to the Netherlands.

    February 24, 2014

  • Simon M.

    The lists of meetups planned for this year can be found here: There are still some free slots, so don't feel shy about grabbing them; and don't forget to register for this year's ZuriHac ;-)

    February 24, 2014

10 went

Our Sponsors


    Better sponsors the HaskellerZ meetup account.

People in this
Meetup are also in:

Create a Meetup Group and meet new people

Get started Learn more

I started the group because there wasn't any other type of group like this. I've met some great folks in the group who have become close friends and have also met some amazing business owners.

Bill, started New York City Gay Craft Beer Lovers

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy