Back to Search
Start Over
Formalizing Operational Semantic Specifications in Logic
- Source :
- Electronic Notes in Theoretical Computer Science. 246:147-165
- Publication Year :
- 2009
- Publisher :
- Elsevier BV, 2009.
-
Abstract
- We review links between three logic formalisms and three approaches to specifying operational semantics. In particular, we show that specifications written with (small-step and big-step) SOS, abstract machines, and multiset rewriting, are closely related to Horn clauses, binary clauses, and (a subset of) linear logic, respectively. We shall illustrate how binary clauses form a bridge between the other two logical formalisms. For example, using a continuation-passing style transformation, Horn clauses can be transformed into binary clauses. Furthermore, binary clauses can be seen as a degenerative form of multiset rewriting: placing binary clauses within linear logic allows for rich forms of multiset rewriting which, in turn, provides a modular, big-step SOS specifications of imperative and concurrency primitives. Establishing these links between logic and operational semantics has many advantages for operational semantics: tools from automated deduction can be used to animate semantic specifications; solutions to the treatment of binding structures in logic can be used to provide solutions to binding in the syntax of programs; and the declarative nature of logical specifications provides broad avenues for reasoning about semantic specifications.
- Subjects :
- Horn clause
Theoretical computer science
General Computer Science
Syntax (programming languages)
Programming language
Concurrency
big-step SOS semantics
computer.software_genre
Rotation formalisms in three dimensions
Operational semantics
Abstract machine
Linear logic
Theoretical Computer Science
small-step SOS semantics
Automated theorem proving
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
specifications
computer
multiset rewriting
Computer Science(all)
Mathematics
Subjects
Details
- ISSN :
- 15710661
- Volume :
- 246
- Database :
- OpenAIRE
- Journal :
- Electronic Notes in Theoretical Computer Science
- Accession number :
- edsair.doi.dedup.....f85852ec69b7262c847d649e7a47d6e2