Formal Methods and Crypto in Agda

This workshop will be held at the University Residential Center in the small picturesque town of Bertinoro between May 28 to June 02, 2023.  The workshop will provide a solid foundation in development of programs and proofs in Agda with applications to formal specification of cryptographic protocols.  The workshop will take place over 19 sessions. Most of the sessions will be spent on Agda and Agda Lab sessions; there will be also sessions on ledger models in Agda as well as other short talks. The core of the course will be delivered by Phil Wadler and will use the textbook Programming Language Foundations in Agda.