2 Search Results for "Rose, Kristoffer H."

Document

DOI: 10.4230/LIPIcs.FSCD.2024.11

Optimizing a Non-Deterministic Abstract Machine with Environments

Authors: Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

Non-deterministic abstract machine (NDAM) is a recent implementation model for programming languages where one must choose among several redexes at each reduction step, like process calculi. These machines can be derived from a zipper semantics, a mix between structural operational semantics and context-based reduction semantics. Such a machine has been generated also for the λ-calculus without a fixed reduction strategy, i.e., with the full non-deterministic β-reduction. In that machine, substitution is an external operation that replaces all the occurrences of a variable at once. Implementing substitution with environments is more low-level and more efficient as variables are replaced only when needed. In this paper, we define a NDAM with environments for the λ-calculus without a fixed reduction strategy. We also introduce other optimizations, including a form of refocusing, and we show that we can restrict our optimized NDAM to recover some of the usual λ-calculus machines, e.g., the Krivine Abstract Machine. Most of the improvements we propose in this work could be applied to other NDAMs as well.

Cite as

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.FSCD.2024.11,
  author =	{Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan},
  title =	{{Optimizing a Non-Deterministic Abstract Machine with Environments}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{11:1--11:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.11},
  URN =		{urn:nbn:de:0030-drops-203409},
  doi =		{10.4230/LIPIcs.FSCD.2024.11},
  annote =	{Keywords: Abstract machine, Explicit substitutions, Refocusing}
}

Document

DOI: 10.4230/LIPIcs.RTA.2011.81

CRSX - Combinatory Reduction Systems with Extensions

Authors: Kristoffer H. Rose

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract

Combinatory Reduction Systems with Extensions (CRSX) is a system available from http://crsx.sourceforge.net and characterized by the following properties: - Higher-order rewriting engine based on pure Combinatory Reduction Systems with full strong reduction (but no specified reduction strategy). - Rule and term syntax based on lambda-calculus and term rewriting conventions including Unicode support. - Strict checking and declaration requirements to avoid idiosyncratic errors in rewrite rules. - Interpreter is implemented in Java 5 and usable stand-alone as well as from an Eclipse plugin (under development). - Includes a custom parser generator (front-end to JavaCC parser generator) designed to ease parsing directly into higher-order abstract syntax (as well as permitting the use of custom syntax in rules files). - Experimental (and evolving) sort system to help rule management. - Compiler from (well-sorted deterministic subset of) CRSX to stand-alone C code.

Cite as

Kristoffer H. Rose. CRSX - Combinatory Reduction Systems with Extensions. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 81-90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{rose:LIPIcs.RTA.2011.81,
  author =	{Rose, Kristoffer H.},
  title =	{{CRSX - Combinatory Reduction Systems with Extensions}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{81--90},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.81},
  URN =		{urn:nbn:de:0030-drops-31301},
  doi =		{10.4230/LIPIcs.RTA.2011.81},
  annote =	{Keywords: Higher-Order Rewriting, Compilers}
}

Refine by Author
1 Biernacka, Małgorzata
1 Biernacki, Dariusz
1 Lenglet, Sergueï
1 Rose, Kristoffer H.
1 Schmitt, Alan

Refine by Classification
1 Theory of computation → Abstract machines

Refine by Keyword
1 Abstract machine
1 Compilers
1 Explicit substitutions
1 Higher-Order Rewriting
1 Refocusing

Refine by Type
2 document

Refine by Publication Year
1 2011
1 2024