| dc.contributor.author | Nagele, J | en_US |
| dc.contributor.author | Oostrom, VV | en_US |
| dc.contributor.author | Sternagel, C | en_US |
| dc.contributor.author | 5th International Workshop on Confluence | en_US |
| dc.date.accessioned | 2018-05-10T13:45:20Z | |
| dc.date.available | 2016-07-17 | en_US |
| dc.date.issued | 2016-08-01 | en_US |
| dc.date.submitted | 2018-05-02T17:18:02.367Z | |
| dc.identifier.uri | http://qmro.qmul.ac.uk/xmlui/handle/123456789/37364 | |
| dc.description | 5th International Workshop on Confluence | en_US |
| dc.description | 5th International Workshop on Confluence | en_US |
| dc.description.abstract | We present a short proof of the Church-Rosser property for the lambda-calculus enjoying two distinguishing features: Firstly, it employs the Z-property, resulting in a short and elegant proof; and secondly, it is formalized in the nominal higher-order logic available for the proof assistant Isabelle/HOL. | en_US |
| dc.subject | cs.LO | en_US |
| dc.subject | cs.LO | en_US |
| dc.title | A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle | en_US |
| dc.type | Conference Proceeding | |
| dc.rights.holder | © The Author(s) 2016 | |
| pubs.author-url | http://arxiv.org/abs/1609.03139v1 | en_US |
| pubs.notes | Not known | en_US |
| pubs.publication-status | Published | en_US |
| dcterms.dateAccepted | 2016-07-17 | en_US |
