Your browser seems to have problems showing our website properly so it's switched to a simplified version.
Constructive and Non-Constructive Proofs in Agda (Part 3): Playing with Negation
November 30th, 2018.
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…
Constructive and Non-Constructive Proofs in Agda (Part 2): Agda in a Nutshell
November 26th, 2018.
Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda..
Constructive and Non-Constructive Proofs in Agda (Part 1): Logical Background
November 14th, 2018.
Hi! I’m Danya Rogozin, and I work at Serokell on a blockchain framework called Snowdrop.. I would like to tell you about constructive and non-constructive proofs in a proof assistant and functional …