1 Search Results for "Drab, Tomasz"


Document
The Zoo of Lambda-Calculus Reduction Strategies, And Coq

Authors: Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
We present a generic framework for the specification and reasoning about reduction strategies in the lambda calculus, representable as sets of term decompositions. It is provided as a Coq formalization that features a novel format of phased strategies. It facilitates concise description and algebraic reasoning about properties of reduction strategies. The formalization accommodates many well-known strategies, both weak and strong, such as call by name, call by value, head reduction, normal order, full β-reduction, etc. We illustrate the use of the framework as a tool to inspect and categorize the "zoo" of existing strategies, as well as to discover and study new ones with particular properties.

Cite as

Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The Zoo of Lambda-Calculus Reduction Strategies, And Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7,
  author =	{Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz},
  title =	{{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7},
  URN =		{urn:nbn:de:0030-drops-167165},
  doi =		{10.4230/LIPIcs.ITP.2022.7},
  annote =	{Keywords: Lambda calculus, Reduction strategies, Coq}
}
  • Refine by Author
  • 1 Biernacka, Małgorzata
  • 1 Charatonik, Witold
  • 1 Drab, Tomasz

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 1 Coq
  • 1 Lambda calculus
  • 1 Reduction strategies

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

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