## 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

16 hours 37 min ago

17 hours 26 min ago

23 hours 59 min ago

1 day 1 hour ago

1 day 10 hours ago

1 day 10 hours ago

1 day 10 hours ago

1 day 12 hours ago

1 day 14 hours ago

1 day 17 hours ago