Mihaly Barasz - Practical Intro to Agda and Coq

Public group

Online event

This event has passed


A hands-on, code-along introduction to Agda. We'll go over the basics using our Haskeller goggles, mostly focusing on interactive experimenting and proof development.

I will compare Agda and Coq, again mostly from practical, “UX” standpoint (though I'll say a few words about theoretical differences). And we'll do a bunch of toy examples, which will hopefully illuminate why functional programming has such a deep and intricate relationship with logic and proofs.

The main goal is to give a taste of these two incredible Proof Assistants, get our hands dirty, and for anyone who gets interested to have a pointer to further resources.


I wrote some installation instructions for those of you who'd want to follow along but don't have Agda or Coq set up yet. I also created a Docker image with everything configured properly. The image is a bit heavy (1GB compressed), but is probably the fastest way to get going, and is very easy to clean up afterwards. ;)



This will be an online event. We will be using Zoom for video conference and Slack for chat. The video will be recorded and uploaded to YouTube after the event.

Please join the ZuriHac Slack workspace using the following link and then join the #meetup channel. https://join.slack.com/t/zurihac/shared_invite/zt-edz4ubz9-V4ciNSVdd4YKi3i8eA9PIw
Please join the video conference using the following link. https://us02web.zoom.us/j/89219704744?pwd=aEpRMDR5VVh3Zi9PL2h0Vjh3YWtmdz09
Meeting ID:[masked]