Confluence of an extension of combinatory logic by Boolean constants
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- Confluence of an extension of combinatory logic by Boolean constants
Final published version, 513 KB, PDF document
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.
| Original language | English |
|---|---|
| Title of host publication | 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 |
| Editors | Dale Miller |
| Number of pages | 16 |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Publication date | 1 Sep 2017 |
| Article number | 14 |
| ISBN (Electronic) | 9783959770477 |
| DOIs | |
| Publication status | Published - 1 Sep 2017 |
| Event | 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 - Oxford, United Kingdom Duration: 3 Sep 2017 → 9 Sep 2017 |
Conference
| Conference | 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 |
|---|---|
| Land | United Kingdom |
| By | Oxford |
| Periode | 03/09/2017 → 09/09/2017 |
| Series | Leibniz International Proceedings in Informatics |
|---|---|
| Volume | 84 |
| ISSN | 1868-8969 |
- Combinatory logic, Conditional linearization, Confluence, Unique normal form property
Research areas
Number of downloads are based on statistics from Google Scholar and www.ku.dk
No data available
ID: 194818826