01497841

a

01497841 Kang, Kyoung-Sun Tamura, Naoyuki A static analysis method for a classical linear logic programming language. Dutra, In\^es (ed.) et al., Parallelism and implementation technology for (constraint) logic programming. Workshop in conjunction with ICLP '99, Las Cruces, NM, USA, December 1, 1999. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 30,3, 17 p., electronic only (1999). 1999 Amsterdam: Elsevier EN linear logic programming language

http://www.elsevier.com/gej-ng/31/29/23/55/27/show/Products/notes/index.htt#002

Summary: In this paper, we propose a new static analysis method which is applicable for a classical linear logic programming language. Andreoli et al. proposed a static analysis method for the classical linear logic programming language LO, but their method did not cover multiplicative connectives which are important for a resource-sensitive feature of linear logic. Our method, in contrast, covers multiplicative conjunction in addition to multiplicative disjunction and linear implication. An abstract proof graph, an AND-OR graph representing all possible sequent proofs, is constructed from a given program and goal sequent. The graph can be repeatedly refined by propagating information to eliminate unprovable nodes from the graph. We applied our prototype analyzer for a sorting program written in Forum. The sorting program was improved about 1000 times faster than the ordinary program without analysis, for sorting 6 elements by using the analysis result.