@inproceedings{59708a76735543dda09c752db30e5599,
title = "Confluence of an extension of combinatory logic by Boolean constants",
abstract = "We show confluence of a conditional term rewriting system CL-pc1, 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.",
keywords = "Combinatory logic, Conditional linearization, Confluence, Unique normal form property",
author = "{\L}ukasz Czajka",
year = "2017",
month = sep,
day = "1",
doi = "10.4230/LIPIcs.FSCD.2017.14",
language = "English",
series = "Leibniz International Proceedings in Informatics",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Dale Miller",
booktitle = "2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017",
note = "2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 ; Conference date: 03-09-2017 Through 09-09-2017",
}