  Agda is a dependently-typed functional programming language, based on an
extension of intuitionistic Martin-L\"of type theory. We implement first order
natural deduction in Agda. We use Agda's type checker to verify the correctness
of natural deduction proofs, and also prove properties of natural deduction,
using Agda's proof assistant functionality. This implementation corresponds to
a formalisation of natural deduction in constructive type theory, and the
proofs are verified by Agda to be correct (under the assumption that Agda
itself is correct).
