A computational interpretation of modal proofs