5 citations · 13 across the 7 of their papers we have counts for
7 papers · 1 filter
Blockchain Superoptimizer
Julian Nagele, Maria A Schett
In the blockchain-based, distributed computing platform Ethereum, programs called smart contracts are compiled to bytecode and executed on the Ethereum Virtual Machine (EVM). Execu…
Confluence by Critical Pair Analysis Revisited (Extended Version)
Nao Hirokawa, Julian Nagele, Vincent van Oostrom +1
We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule label…
Critical Peaks Redefined -
Nao Hirokawa, Julian Nagele, Vincent van Oostrom +1
Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as p…
CoCoWeb - A Convenient Web Interface for Confluence Tools
Julian Nagele, Aart Middeldorp
We present a useful web interface for tools that participate in the annual confluence competition.
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…
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…
Certification of Confluence Proofs using CeTA
Julian Nagele, René Thiemann
CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, th…