4 ms·

Non termination is modeled as false: a function that takes an A and never terminates has type A -> F, or ~A. There's some connection between classical logics a

by mkehrt 10y ago

Non termination is modeled as false: a function that takes an A and never terminates has type A -> F, or ~A. There's some connection between classical logics and concurrency, though it's hard to get at. You can use callcc to implement threads, and Getzen's classical sequent calculus has multiple conclusions. Here is a PHD thesis that uses modal logic to model distributed code in a CH fashion: http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-code.pdf http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-co... Classical logic is perfectly modeled with callcc, which has the type Peirce's Law, and allows one to write terms with the types of the law of excluded middle or Double Negation Elimination.

mafribe 10y ago
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.