Searching for semantics

ABSTRACT

We consider the task of generating operational semantics, defined as axiomatizations of relations such as e → v, from an equality theory, given as a set of equations {e1 = e2}. We generate these semantics by constructing derived rules based on equations provable in this equality theory and constrained by a simple correctness criteria. This criteria, which we have previously used in verifying compiler correctness, states that the generated semantics correctly implements a given source language. We use Elf, a logic programming language, to axiomatize source language semantics, equality theories for target languages, and translations between source and target languages, and to construct the derived rules, based on these axiomatizations, for the target languages. During the process of constructing derived rules we simultaneously construct a correctness proof, relating these new rules to a given source language and the translation between languages. Previous uses of Elf (in compiler construction and language manipulation) have focused on the language's type system to express statements of correctness. We focus here on Elf's search paradigm, exploiting it in a crucial way to construct objects representing semantic specifications. We have only considered operational semantics for simple functional languages, but we expect that our results can be generalized to a wider class of languages.

REFERENCES

• 1: M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L~vy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.
• 2: Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Levy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.
• 3: Rod Burstall , Furio Honsell, Operational semantics in a natural deduction setting, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 4: Thierry Coquand, An algorithm for testing conversion in type theory, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 5: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• 6: Pierre-Louis Curien. The Ap-calculus: An abstract framework for environment machines. Technical report, LIENS-CNRS, 1990.
• 7: Jo~lle Despeyroux. Proof of translation in natural semantics. In Proceedings of the First IEEE Symposium on Logic in Computer Science, pages 193-205, Cambridge, Massachusetts, 1986. IEEE Computer Society Press.
• 8: John Hannan, Staging transformations for abstract machines, Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.130-141, June 17-19, 1991, New Haven, Connecticut, United States
• 9: J. Hannan , D. Miller, A meta-logic for functional programming, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
• 10: John I-Iannan ,and Frank Pfenning. Compiler verification in LF. In Andre Scedrov, editor, Proceedings of the Seventh Annual 1EEE Symposium on Logic in Computer Science.~ pages 407-418. IEEE Computer Society Press, 1992.
• 11: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 12: G. Kahn, Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, p.22-39, February 1987, Passau, Germany
• 13: Spiro Michaylov , Frank Pfenning, Natural semantics and some of its meta-theory in Elf, Conference Proceedings on Extensions of logic programming, p.299-344, January 1992, Stockholm, Sweden
• 14: Dale Miller. A logic programming language with lambda-abstracl,ion, function variables, and simple unification. Journal of Logic and Computation, 1(4):497- 536, 1991.
• 15: F. Pfening, Elf: a language for logic definition and verified metaprogramming, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.313-322, June 1989, Pacific Grove, California, United States
• 16: Frank Pfenning. An implementation of the Elf core language in Standard ML. Available via ftp over the internet, September 1991. Send mail to [e-mail] for further information.
• 17: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 18: Frank Pfenning , Ekkehard Rohwedder, Implementing the Meta-Theory of Deductive Systems, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.537-551, June 15-18, 1992

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Languages, Theory, Verification