## User login## Navigation |
## Translation of Tree-processing Programs into Stream-processing Programs based on Ordered Linear TypesTranslation of Tree-processing Programs into Stream-processing Programs based on Ordered Linear Types, Koichi Kodama, Kohei Suenaga, Naoki Kobayashi, JFP 2008.
Linear logic is what you get when you give up the structural rules of weakening and contraction -- it's logic when you cannot reuse or forget any hypothesis you make in the course of a proof. This means that every formula is used exactly once, which makes it useful (via Curry-Howard) for programming, as well: linear types give us a way of tracking resources and state in a type system. Intuitively, you can think of it as a kind of static analysis that ensures that an object's runtime reference count will always be one. However, linear logic retains the structural rule of exchange, which lets us use hypotheses in a different order than we introduced them. Ordered logic is what you get when you drop exchange, as well. (Amusingly, it was invented long before linear logic -- in the 1950s, Lambek introduced it with an eye towards applications in linguistics: he wanted to express the difference between one word occurring either before, or after, another.) This means that you can use ordered logic to express the order in your types the |
## Browse archives## Active forum topics |

## Recent comments

4 days 5 hours ago

5 days 45 min ago

5 days 4 hours ago

5 days 5 hours ago

5 days 6 hours ago

5 days 6 hours ago

5 days 7 hours ago

5 days 7 hours ago

5 days 11 hours ago

5 days 12 hours ago