From big-step to small-step semantics and back with interpreter specialisation

Gallagher, John P. and Hermenegildo, Manuel V. and Kafle, Bishoksan and Klemen, Maximiliano and López García, Pedro and Morales Caballero, José Francisco (2020). From big-step to small-step semantics and back with interpreter specialisation. In: "8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis (VPT/HCVS@ETAPS 2020)", 25-26 Abr 2020, Dublín, Irlanda. pp. 50-64. https://doi.org/10.4204/EPTCS.320.4.

Description

Title: From big-step to small-step semantics and back with interpreter specialisation
Author/s:
  • Gallagher, John P.
  • Hermenegildo, Manuel V.
  • Kafle, Bishoksan
  • Klemen, Maximiliano
  • López García, Pedro
  • Morales Caballero, José Francisco
Item Type: Presentation at Congress or Conference (Article)
Event Title: 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis (VPT/HCVS@ETAPS 2020)
Event Dates: 25-26 Abr 2020
Event Location: Dublín, Irlanda
Title of Book: Proceedings of VPT/HCVS@ETAPS 2020 : 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
Date: 2020
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (223kB) | Preview

Abstract

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

More information

Item ID: 65444
DC Identifier: http://oa.upm.es/65444/
OAI Identifier: oai:oa.upm.es:65444
DOI: 10.4204/EPTCS.320.4
Official URL: http://eptcs.web.cse.unsw.edu.au/paper.cgi?VPTHCVS2020.4.pdf
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 17 Nov 2020 08:40
Last Modified: 17 Nov 2020 08:40
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM