I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at?
Here are some further details. I have a simple proof checker for propositional calculus implemented in Lean (see this and this). I am hoping to do the same for predicate logic. I then intend to create a proof assistant in Haskell and have the proofs created using it be exportable to a format that can be run through the Lean implementation of the checker. In this manner I hope to have a formal proof of the soundness of the trusted kernel, assuming that Lean is sound. The current state of this is here.
The issue at present is deciding if I should change to a different encoding for variables, for example locally nameless. The simplest to implement seems to be the substitution described here, but I am not certain if it has shortcomings that I have not seen yet.