Non termination is modeled as false: That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whats

Non termination is modeled as false: That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whatsoever of interest (from a specifiation and verification point of view) about non-terminating computation. The T. Murphy PhD doesn't deal with distribution because it lacks the key feature of distribution which is partial failure. As far as I'm aware the work on modelling double negation by call/cc doesn't actually provide a 1-to-1 correspondence between programs and proofs. I've forgotten the details but I think only some programs come out being proofs.