Linear logical approximations

ABSTRACT

The abstract interpretation of programs relates the exact semantics of a programming language to an approximate semantics that can be effectively computed. We show that, by specifying operational semantics in a bottom-up, linear logic programming language -- a technique we call "substructural operational semantics" (SSOS) -- manifestly sound program approximations can be derived by simple and intuitive approximations of the logic program. As examples, we describe how to derive a simple alias analysis, 0CFA, and kCFA analysis from a substructural operational semantics of the relevant languages.

REFERENCES

• 1: Alfred V. Aho , Monica S. Lam , Ravi Sethi , Jeffrey D. Ullman, Compilers: Principles, Techniques, and Tools (2nd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 2: Marco Bozzano , Giorgio Delzanno, Automated protocol verification in linear logic, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.38-49, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571162]
• 3: Marco Bozzano , Giorgio Delzanno , Maurizio Martelli, An effective fixpoint semantics for linear logic programs, Theory and Practice of Logic Programming, v.2 n.1, p.85-122, January 2002 [doi>10.1017/S1471068402001254]
• 4: Marco Bozzano , Giorgio Delzanno , Maurizio Martelli, Model checking linear logic specifications, Theory and Practice of Logic Programming, v.4 n.5-6, p.573-619, September 2004 [doi>10.1017/S1471068404002066]
• 5: Iliano Cervesato , Andre Scedrov, Relating State-Based and Process-Based Concurrency through Linear Logic, Electronic Notes in Theoretical Computer Science (ENTCS), 165, p.145-176, November, 2006 [doi>10.1016/j.entcs.2006.05.043]
• 6: Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins. A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-02-102, School of Computer Science, Carnegie Mellon University, March 2002. Revised May 2003.
• 7: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 8: Cormac Flanagan , Amr Sabry , Bruce F. Duba , Matthias Felleisen, The essence of compiling with continuations, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.237-247, June 21-25, 1993, Albuquerque, New Mexico, United States
• 9: Harald Ganzinger , David A. McAllester, Logical Algorithms, Proceedings of the 18th International Conference on Logic Programming, p.209-223, July 29-August 01, 2002
• 10: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 11: Joshua S. Hodas , Dale Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation, v.110 n.2, p.327-365, May 1, 1994

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Design, Languages, Theory

Keywords:
abstract interpretation, bottom-up linear logic programming, operational semantics