Search Results

Documents authored by Schmitt, Alan

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.CONCUR.2022.7
Non-Deterministic Abstract Machines

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

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We present a generic design of abstract machines for non-deterministic programming languages, such as process calculi or concurrent lambda calculi, that provides a simple way to implement them. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way. We show how to automatically derive a non-deterministic abstract machine from a zipper semantics - a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics.
Cite as

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Non-Deterministic Abstract Machines. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.CONCUR.2022.7,
  author =	{Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan},
  title =	{{Non-Deterministic Abstract Machines}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{7:1--7:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.7},
  URN =		{urn:nbn:de:0030-drops-170705},
  doi =		{10.4230/LIPIcs.CONCUR.2022.7},
  annote =	{Keywords: Abstract machines, non-determinism, lambda-calculus, process calculi}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.212
Howe's Method for Contextual Semantics

Authors: Serguei Lenglet and Alan Schmitt

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We show how to use Howe's method to prove that context bisimilarity is a congruence for process calculi equipped with their usual semantics. We apply the method to two extensions of HOpi, with passivation and with join patterns, illustrating different proof techniques.
Cite as

Serguei Lenglet and Alan Schmitt. Howe's Method for Contextual Semantics. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 212-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{lenglet_et_al:LIPIcs.CONCUR.2015.212,
  author =	{Lenglet, Serguei and Schmitt, Alan},
  title =	{{Howe's Method for Contextual Semantics}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{212--225},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.212},
  URN =		{urn:nbn:de:0030-drops-53642},
  doi =		{10.4230/LIPIcs.CONCUR.2015.212},
  annote =	{Keywords: Bisimulation, process calculi, Howe's method}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact