Found people interested in #OpenGenera, anyone interested in #Nuprl or #MetaPRL, the dependent type theory theorem prover? One year before I have got MetaPRL working with recent version of OCaml, but did not have enough knowledge and time to continue the development.