Correspondence assertions are used as a means to express authentication properties in communicating protocols expressed in the pi and Spi-calculi. A protocol is considered safe if assertions in the protocol always hold. It has been shown by Gordon and Jeffrey that a type system can provide a sound approximation to the safety property. A paper by Hüttel shows that sound and complete type inference for such a system can be achieved by encoding constraints to a subset of propositional logic, ALFP, which can be satisfied by the Succinct Solver, a tool developed by Nielson, Nielson and Seidl. In 2007, Fournet, Gordon and Maffeis generalised the notion of correspondence assertions by using Datalog, a logic programming language utilising a subset of ALFP, and developed a type system for verifying these assertions. An existing implementation of the type system with Datalog correspondences was mentioned, but apparantly not published. Likewise, the type inference method of Hüttel has not seen an actual implementation yet. We aim to implement a type checker for the type system with Datalog correspondences, as presented by Fournet, Gordon and Maffeis. We also aim to implement the type inference method for a type system with non-injective correspondences, as presented by Hüttel. We use Objective Caml for both implementations. For the type checker implementation, the Succinct Solver is used to interpret the Datalog correspondences, as Datalog logic expressions are a subset of ALFP. For the type inference implementation, the Succinct Solver is used as the last stage of the inference algorithm. We prove that the algorithm used to implement the type checker is sound and complete. We provide a few correctly typed examples with the type checker. We do not complete the type inference implementation. But we provide a partial implementation as a framework for a complete implementation of the method. We point to issues with the method and show how they can be, or might be, solved.