Sciweavers

RTA
2015
Springer
8 years 8 months ago
Leftmost Outermost Revisited
We present an elementary proof of the classical result that the leftmost outermost strategy is normalizing for left-normal orthogonal rewrite systems. Our proof is local and exten...
Nao Hirokawa, Aart Middeldorp, Georg Moser
RTA
2015
Springer
8 years 8 months ago
Formalizing Bialgebraic Semantics in PVS 6.0
Both operational and denotational semantics are prominent approaches for reasoning about properties of programs and programming languages. In the categorical framework developed b...
Sjaak Smetsers, Ken Madlener, Marko C. J. D. van E...
RTA
2015
Springer
8 years 8 months ago
Head reduction and normalization in a call-by-value lambda-calculus
Recently, a standardization theorem has been proven for a variant of Plotkin’s call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this ...
Giulio Guerrieri
RTA
2015
Springer
8 years 8 months ago
Transforming Cycle Rewriting into String Rewriting
We present new techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main techni...
David Sabel, Hans Zantema
RTA
2015
Springer
8 years 8 months ago
No complete linear term rewriting system for propositional logic
Recently it has been observed that the set of all sound linear inference rules in propositional logic is already coNP-complete, i.e. that every boolean tautology can be written as...
Anupam Das, Lutz Straßburger
RTA
2015
Springer
8 years 8 months ago
Presenting a Category Modulo a Rewriting System
Presentations of categories are a well-known algebraic tool to provide descriptions of categories by the means of generators, for objects and morphisms, and relations on morphisms...
Florence Clerc, Samuel Mimram
RTA
2015
Springer
8 years 8 months ago
Matrix Interpretations on Polyhedral Domains
We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities...
Johannes Waldmann
RTA
2015
Springer
8 years 8 months ago
Network Rewriting II: Bi- and Hopf Algebras
Bialgebras and their specialisation Hopf algebras are algebraic structures that challenge traditional mathematical notation, in that they sport two core operations that defy the b...
Lars Hellström
RTA
2015
Springer
8 years 8 months ago
Observing Success in the Pi-Calculus
A contextual semantics – defined in terms of successful termination and may- and shouldconvergence – is analyzed in the synchronous pi-calculus with replication and a constan...
David Sabel, Manfred Schmidt-Schauß
RTA
2015
Springer
8 years 8 months ago
A faithful encoding of programmable strategies into term rewriting systems
Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transfo...
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etie...