User loginNavigation |
archivesTyped Process CalculiIf Curry-Howard is your thing, you'll like this: Propositions as Sessions by Philip Wadler.
I was unable to find much LTU discussion about session types; they express the protocol that a process speaks over a channel [conjunction describes multistep conversations; disjunction offers a choice between different interactions, e.g. buy an item vs. quote its price --- you can see the type for this in Caires and Pfenning]. Instead of applying functions, one creates a channel and puts processes on either end of it. The types ensure that when one side of the channel is pushing output, the other side is reading input. This dual relationship between input/output corresponds with the dual (linear negation) in linear logic. Proof reduction (cut elimination) simulates communication between processes.
|
Browse archivesActive forum topics |
Recent comments
1 day 15 hours ago
1 day 19 hours ago
1 day 19 hours ago
22 weeks 3 days ago
26 weeks 4 days ago
28 weeks 2 days ago
28 weeks 2 days ago
30 weeks 6 days ago
35 weeks 4 days ago
35 weeks 4 days ago