Post #2728850

I'm not sure if this is too specific a question for anyone to answer, but here goes. I've recently been looking into Krivine's proof of a variant of the completeness theorem for classical first order logic. In the paper "Krivine’s intuitionistic proof of classical completeness (for countable languages)", Berardo and Valentini say: > It is a bit puzzling that, even if Krivine’s algorithm was recently implemented by Raffalli, no explicit description of it is currently available. Does anybody know what this could be referring to? I've gathered that they're probably talking about Christophe Raffalli, but I haven't been able to find more than that. I've been working on a formalization of Krivine's paper myself and it would be nice to see what kind of implementation work has already been done.