Searching for semantics

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
Editors Anon
PublisherPubl by ACM
Pages1-12
Number of pages12
ISBN (Print)0897915941
StatePublished - 1993
EventProceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation - Copenhagen, Den
Duration: Jun 14 1993Jun 16 1993

Other

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

Fingerprint

Semantics
Logic programming
Computer programming languages
Specifications

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Hannan, J. J. (1993). Searching for semantics. In Anon (Ed.), Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation (pp. 1-12). Publ by ACM.
Hannan, John Joseph. / Searching for semantics. Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation. editor / Anon. Publ by ACM, 1993. pp. 1-12
@inproceedings{0019ec0b487743119aea8339f30a826b,
title = "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.",
author = "Hannan, {John Joseph}",
year = "1993",
language = "English (US)",
isbn = "0897915941",
pages = "1--12",
editor = "Anon",
booktitle = "Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation",
publisher = "Publ by ACM",

}

Hannan, JJ 1993, Searching for semantics. in Anon (ed.), Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation. Publ by ACM, pp. 1-12, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, Copenhagen, Den, 6/14/93.

Searching for semantics. / Hannan, John Joseph.

Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation. ed. / Anon. Publ by ACM, 1993. p. 1-12.

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

TY - GEN

T1 - Searching for semantics

AU - Hannan, John Joseph

PY - 1993

Y1 - 1993

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0027866007&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0027866007&partnerID=8YFLogxK

M3 - Conference contribution

SN - 0897915941

SP - 1

EP - 12

BT - Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation

A2 - Anon, null

PB - Publ by ACM

ER -

Hannan JJ. Searching for semantics. In Anon, editor, Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation. Publ by ACM. 1993. p. 1-12