Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.

Peter Chapman, James McKinna, Christian Urban

Browse the full AISC paper archive.