Blog: Formal Verification
![formal verification thumbnail](/files/cy/thumb.cyqo6e2c.thumbnail3_(1).jpg)
![formal verification thumbnail](/files/9f/thumb.9fvka1ta.formal-verification.jpg)
Formal Verification: History and Methods
In the first part of our series about formal verification, we discuss the roots of formal verification in fields such as mathematical logic and theoretical computer science.
![Agda: Playing With Negation](/files/8j/thumb.8j0246ad.agda-fb.jpg)
![Agda: Playing With Negation](/files/a5/thumb.a5oggzbc.constructive-and-non-constrictive3.jpg)
Constructive and Non-Constructive Proofs in Agda (Part 3): Playing with Negation
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…
![Agda in a nutshell](/files/0h/thumb.0hvaw086.agda-fb_(1).jpg)
![Agda in a nutshell](/files/iq/thumb.iq4j1g8l.constructive-and-non-constrictive2.jpg)
Constructive and Non-Constructive Proofs in Agda (Part 2): Agda in a Nutshell
Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda..
![Agda: Logical Background](/files/o9/thumb.o9t1nw19.agda-fb.jpg)
![Agda: Logical Background](/files/tw/thumb.tw9u4t8s.constructive-and-non-constrictive.jpg)
Constructive and Non-Constructive Proofs in Agda (Part 1): Logical Background
Where to start with Agda formal verification? Get familiar with the constructive logic behind it.