ACL2 Seminar, Feb. 1, 2019

Speaker: Curtis Dunham

Title: "An Introduction To Agda"

Abstract:
Agda is a programming and proof system based on dependent types.  The talk
will be split between a theoretical lecture covering Agda's foundations,
history, and academic neighborhood followed by or interleaved with a more
practical code tour and demonstration.  The goal is to give the audience a
useful introduction to the system, including its strengths and weaknesses
and how it feels to use as a proof assistant.