5 citations · 13 across the 7 of their papers we have counts for
Showing 2016Show all
2 papers · 1 filter
cs.LO2016★ 1 cited
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Julian Nagele, Bertram Felgenhauer, Harald Zankl
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based o…
cs.LO2016★ 1 cited
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the -calculus in Nominal Isabelle
Julian Nagele, Vincent van Oostrom, Christian Sternagel
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 el…