I am planning to implement a FOL proof assistant in Haskell, what are some useful libraries and implementations I should be looking at?

EDIT

Further details:

I have a simple proof checker for propositional calculus implemented in Lean [1]. 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 [2].

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 [3], but I am not certain if it has shortcomings that I have not seen yet.

[1a] https://github.com/pthomas505/lean3/blob/ecb551d720f88bc0c8662e218e6285db9593272f/src/metalogic/check_prop.lean

[1b] https://github.com/pthomas505/lean3/blob/ecb551d720f88bc0c8662e218e6285db9593272f/src/metalogic/prop.lean

[2] https://github.com/pthomas505/lean3/blob/ecb551d720f88bc0c8662e218e6285db9593272f/src/metalogic/pred.lean

[3] http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html

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.

I am planning to implement a FOL proof assistant in Haskell, what are some useful libraries and implementations I should be looking at?

I am planning to implement a FOL proof assistant in Haskell, what are some useful libraries and implementations I should be looking at?

EDIT

Further details:

I have a simple proof checker for propositional calculus implemented in Lean [1]. 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 [2].

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 [3], but I am not certain if it has shortcomings that I have not seen yet.

[1a] https://github.com/pthomas505/lean3/blob/ecb551d720f88bc0c8662e218e6285db9593272f/src/metalogic/check_prop.lean

[1b] https://github.com/pthomas505/lean3/blob/ecb551d720f88bc0c8662e218e6285db9593272f/src/metalogic/prop.lean

[2] https://github.com/pthomas505/lean3/blob/ecb551d720f88bc0c8662e218e6285db9593272f/src/metalogic/pred.lean

[3] http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html