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.14
URN: urn:nbn:de:0030-drops-77368
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7736/
Go to the corresponding LIPIcs Volume Portal

Czajka, Lukasz

Confluence of an Extension of Combinatory Logic by Boolean Constants

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

Abstract

We show confluence of a conditional term rewriting system CL-pc^1, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalized in the Coq proof assistant.

BibTeX - Entry

@InProceedings{czajka:LIPIcs:2017:7736,
  author =	{Lukasz Czajka},
  title =	{{Confluence of an Extension of Combinatory Logic by Boolean Constants}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{14:1--14:16},
  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/7736},
  URN =		{urn:nbn:de:0030-drops-77368},
  doi =		{10.4230/LIPIcs.FSCD.2017.14},
  annote =	{Keywords: combinatory logic, conditional linearization, unique normal form property, confluence}
}

Keywords: combinatory logic, conditional linearization, unique normal form property, confluence
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