Searching for semantics

John Hannan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation
PublisherPubl by ACM
Pages1-12
Number of pages12
ISBN (Print)0897915941, 9780897915946
DOIs
StatePublished - 1993
EventProceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation - Copenhagen, Den
Duration: Jun 14 1993Jun 16 1993

Publication series

NameProc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation

Other

OtherProceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
CityCopenhagen, Den
Period6/14/936/16/93

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint

Dive into the research topics of 'Searching for semantics'. Together they form a unique fingerprint.

Cite this