License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.10
URN: urn:nbn:de:0030-drops-77188
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7718/
Go to the corresponding LIPIcs Volume Portal

Biernacka, Malgorzata ; Charatonik, Witold ; Zielinska, Klara

Generalized Refocusing: From Hybrid Strategies to Abstract Machines

pdf-format:
LIPIcs-FSCD-2017-10.pdf (0.5 MB)

Abstract

We present a generalization of the refocusing procedure that provides a generic method for deriving an abstract machine from a specification of a reduction semantics satisfying simple initial conditions. The proposed generalization is applicable to a class of reduction semantics encoding hybrid strategies as well as uniform strategies handled by the original refocusing method. The resulting machine is proved to correctly trace (i.e., bisimulate in smaller steps) the input reduction semantics. The procedure and the correctness proofs have been formalized in the Coq proof assistant.

BibTeX - Entry

@InProceedings{biernacka_et_al:LIPIcs:2017:7718,
  author =	{Malgorzata Biernacka and Witold Charatonik and Klara Zielinska},
  title =	{{Generalized Refocusing: From Hybrid Strategies to Abstract Machines}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7718},
  URN =		{urn:nbn:de:0030-drops-77188},
  doi =		{10.4230/LIPIcs.FSCD.2017.10},
  annote =	{Keywords: reduction semantics, abstract machines, formal verification, Coq}
}

Keywords: reduction semantics, abstract machines, formal verification, Coq
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI