Femke van Raamsdonk
Proceedings of the 24th International Conference on Rewriting Techniques and Applications
RTA, 2013.

@proceedings{RTA-2013,
	address       = "Eindhoven, The Netherlands",
	editor        = "Femke van Raamsdonk",
	isbn          = "978-3-939897-53-8",
	publisher     = "{Schloss Dagstuhl — Leibniz-Zentrum für Informatik}",
	series        = "{Leibniz International Proceedings in Informatics}",
	title         = "{Proceedings of the 24th International Conference on Rewriting Techniques and Applications}",
	volume        = 21,
	year          = 2013,
}

Contents (24 items)

3 ×#complexity
3 ×#logic
3 ×#normalisation
2 ×#automation
2 ×#decidability
2 ×#diagrams
2 ×#linear
2 ×#order
2 ×#proving
2 ×#term rewriting

RTA-2013-Kari #automaton #generative

Pattern Generation by Cellular Automata (JK), pp. 1–3.

RTA-2013-Okada #multi #term rewriting

Husserl and Hilbert on Completeness and Husserl’s Term Rewrite-based Theory of Multiplicity (MO), pp. 4–19.

RTA-2013-VytiniotisJ #normalisation

Evidence Normalization in System FC (DV, SLPJ), pp. 20–38.

RTA-2013-Accattoli #linear #logic #normalisation

Linear Logic and Strong Normalization (BA), pp. 39–54.

RTA-2013-AvanziniM #complexity #framework

A Combination Framework for Complexity (MA, GM), pp. 55–70.

RTA-2013-AvanziniM13a #complexity

Tyrolean Complexity Tool: Features and Usage (MA, GM), pp. 71–80.

RTA-2013-BaeEM #infinity #logic #model checking #using

Abstract Logical Model Checking of Infinite-State Systems Using Narrowing (KB, SE, JM), pp. 81–96.

RTA-2013-BauLNW #analysis #term rewriting #termination

Compression of Rewriting Systems for Termination Analysis (AB, ML, EN, JW), pp. 97–112.

RTA-2013-BaumgartnerKLV #anti #higher-order

A Variant of Higher-Order Anti-Unification (AB, TK, JL, MV), pp. 113–127.

RTA-2013-BoichutCR #approximate

Over-approximating Descendants by Synchronized Tree Languages (YB, JC, PR), pp. 128–142.

RTA-2013-Calves #unification

Unifying Nominal Unification (CC), pp. 143–157.

RTA-2013-Das #linear #logic

Rewriting with Linear Inferences in Propositional Logic (AD), pp. 158–173.

RTA-2013-FelgenhauerO #diagrams #order #proving

Proof Orders for Decreasing Diagrams (BF, VvO), pp. 174–189.

RTA-2013-FujitaS #decidability

Decidable structures between Church-style and Curry-style (KeF, AS), pp. 190–205.

RTA-2013-GrabmayerR #λ-calculus #μ-calculus

Expressibility in the λ Calculus with μ (CG, JR), pp. 206–222.

RTA-2013-GuiraudMM #monad #topic

A Homotopical Completion Procedure with Applications to Coherence of Monoids (YG, PM, SM), pp. 223–238.

RTA-2013-Schmidt-SchaussMS #lazy evaluation #λ-calculus

Extending Abramsky’s Lazy λ Calculus: (Non)-Conservativity of Embeddings (MSS, EM, DS), pp. 239–254.

RTA-2013-Schmidt-SchaussRS #algorithm #complexity

Algorithms for Extended α-Equivalence and Complexity (MSS, CR, DS), pp. 255–270.

RTA-2013-SmolkaT #recursion #unification

Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification (GS, TT), pp. 271–286.

RTA-2013-SternagelT #formal method #order

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion (CS, RT), pp. 287–302.

RTA-2013-TushkanovaRGK #automation #calculus #decidability

Automatic Decidability: A Schematic Calculus for Theories with Counting Operators (ET, CR, AG, OK), pp. 303–318.

RTA-2013-WinklerM #normalisation #revisited

Normalized Completion Revisited (SW, AM), pp. 319–334.

RTA-2013-WinklerZM #automation #proving #sequence #termination

Beyond Peano Arithmetic — Automatically Proving Termination of the Goodstein Sequence (SW, HZ, AM), pp. 335–351.

RTA-2013-Zankl #confluence #diagrams

Confluence by Decreasing Diagrams — Formalized (HZ), pp. 352–367.