Indexed linear logic and higher-order model checking
In recent work, Kobayashi observed that the acceptance by an alternating tree automaton A of an infinite tree T generated by a higher-order recursion scheme G may be formulated as the typability of the recursion scheme G in an appropriate intersection type system associated to the automaton A. The p...
| Egile Nagusiak: | , |
|---|---|
| Formatua: | Artikulua |
| Hizkuntza: | English |
| Argitaratua: |
Open Publishing Association
2015-03-01
|
| Saila: | Electronic Proceedings in Theoretical Computer Science |
| Sarrera elektronikoa: | http://arxiv.org/pdf/1503.04909v1 |