Blog: Agda

In this month’s episode of Functional Futures, our guest is David Christiansen – the Executive Director of the Haskell Foundation and the co-author of The Little Typer, a book on dependent types.

In the previous post, we briefly introduced the reader to dependently typed programming and theorem proving in Agda. Now we present an empty type to work with constructive negation. We discuss Marko…

Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda..

Where to start with Agda formal verification? Get familiar with the constructive logic behind it.