You got Agda in my Haskell? By Ryan Orendorff

This event will be streamed on Twitch (please log into twitch before the event starts). Once you RSVP you will see the link to twitch to join!
For the hallway track and to ask the speakers question you can use the chat on Twitch or join our Channel on Matrix.
Any questions about the event please ask in our channel on Matrix. Thank you.

You got Agda in my Haskell?

One of your coworkers seems to write the most amazing Haskell code. It never breaks and it always fits the requirements precisely. You’ve never seen your coworker put in a bug fix for their code ever. One day you decide to ask them how they obtained these inhuman powers. With a huge grin on their face, they say “why that’s because I wrote all my provably correct code in Agda!”

In this talk, we will talk about a new tool called agda2hs which allows programmers to translate dependently typed Agda code into clean Haskell code, enabling the extraction of provably correct programs. We will look into specific examples on how the code can be used to prove that a piece of code has some desired specification such as invertibility.

About our speaker

Hi! My name is Ryan Orendorff, and I enjoy working on type theory, functional programming, linear algebra, and data privacy. If I am not working on those things you can likely find me on a mountain somewhere.

Agenda (Pacific Time)

• 10.00am - Welcome to SF Haskell by Salar Rahmanian
• 10.10am - You got Agda in my Haskell? By Ryan Orendorff

Resources

• For more information about our meetup group (including code of conduct) visit: https://www.sfhaskell.com/
• Follow our twitter channel: https://twitter.com/sf_haskell
• For recordings of talks at our meetup visit our PeerTube: https://watch.softinio.com/c/softinio/videos
• The recordings of talks at our meetup are also available on YouTube: SF Haskell YouTube