TY - GEN
T1 - Searching for semantics
AU - Hannan, John
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
U2 - 10.1145/154630.154631
DO - 10.1145/154630.154631
M3 - Conference contribution
AN - SCOPUS:0027866007
SN - 0897915941
SN - 9780897915946
T3 - Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation
SP - 1
EP - 12
BT - Proc ACM SIGPLAN Symp Partial Eval Semantics Based Program Manipulation
PB - Publ by ACM
T2 - Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
Y2 - 14 June 1993 through 16 June 1993
ER -