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

7 weeks 1 day ago

7 weeks 3 days ago

7 weeks 4 days ago

14 weeks 4 days ago

20 weeks 2 days ago

20 weeks 3 days ago

21 weeks 2 days ago

24 weeks 18 hours ago

25 weeks 3 days ago

25 weeks 4 days ago