Well, the title says it all. The paper describes an implementation in Agda of Valiant’s algorithm. Agda is a typed functional programming language with support for correctness proofs. Valiant’s algorithm is the classic general parsing algorithm for context-free grammars. The algorithm itself is based on a simplified form of context-free grammars (Chomsky Normal Form) and it is not used for parsing real-life programming languages. However, its simplicity and easy algebraic formalization makes it suitable for research, extensions and generalizations. The paper refers to previous work on implementing other algorithms in Agda. There is a reference to [A. Bååth Sjöblom, An Agda proof of the correctness of Valiant’s algorithm for context free parsing. Gothenburg: Chalmers University of Technology (MSc Thesis) (2013)] which does basically the same thing. The authors clarify that the thesis was done under their supervision and this work is a complete rework of the thesis. The paper is structured into three main parts. In the first part, Valiant’s algorithm is homomorphically mapped into the transitive closure over a set of matrices of grammar symbols. The idea is to go along the program of a specification approach. The second part is a short introduction to syntax and concepts of Agda. This language tutorial is followed by a third section that contains the implementation of the algorithm in Agda and all the formal development. The last part is devoted to related work, possible extensions, etc. The paper tries to be self-contained as much as possible; nevertheless, the reader needs to be familiar with typed lambda calculus, functional programming and the Agda language itself in order to get a good grip of the third part. The work is addressed at computer science researchers and professionals interested in program correctness and case use of the Agda system.