English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We investigate representations of imperative programs as constrained Hornclauses. Starting from operational semantics transition rules, we proceed bywriting interpreters as constrained Horn clause programs directly encoding therules. We then specialise an interpreter with respect to a given source programto achieve a compilation of the source language to Horn clauses (an instance ofthe first Futamura projection). The process is described in detail for aninterpreter for a subset of C, directly encoding the rules of big-stepoperational semantics for C. A similar translation based on small-stepsemantics could be carried out, but we show an approach to obtaining asmall-step representation using a linear interpreter for big-step Horn clauses.This interpreter is again specialised to achieve the translation from big-stepto small-step style. The linear small-step program can be transformed back to abig-step non-linear program using a third interpreter. A regular pathexpression is computed for the linear program using Tarjan's algorithm, andthis regular expression then guides an interpreter to compute a program path.The transformation is realised by specialisation of the path interpreter. Inall of the transformation phases, we use an established partial evaluator andexploit standard logic program transformation to remove redundant datastructures and arguments in predicates and rename predicates to make cleartheir link to statements in the original source program.

From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation