There will be a CIRCA seminar on November 2nd, at 1pm in Theatre D of Maths.

Edwin Brady will speak on “The Idris Programming Language”

Details: I will talk about the Idris Programming Language, a language which (like Lean) is based on dependent type theory and (unlike Lean :)) is developed primarily in St Andrews with help from researchers and developers around the world. It is intended for general purpose programming, and supports formal reasoning about those programs. I will give some introductory examples which show how programming and theorem proving interact, and show how we are using dependent type theory to help develop robust and verifiable software.

Jon Fraser will speak on “Fourier analysis in finite fields”.

Details: I will discuss various counting problems in vector spaces over finite fields and show how a ‘Fourier analytic’ approach can help.

All welcome!