Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Biernacka, Malgorzata; Charatonik, Witold; Zielinska, Klara http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-77188
URL:

; ;

Generalized Refocusing: From Hybrid Strategies to Abstract Machines

pdf-format:


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
Seminar: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue date: 2017
Date of publication: 2017


DROPS-Home | Fulltext Search | Imprint Published by LZI