24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@Proceedings{vanraamsdonk:LIPIcs.RTA.2013, title = {{LIPIcs, Volume 21, RTA'13, Complete Volume}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013}, URN = {urn:nbn:de:0030-drops-41152}, doi = {10.4230/LIPIcs.RTA.2013}, annote = {Keywords: Programming Techniques, Software Engineering, Programming Languages, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Artificial Intelligence} }
24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. i-xiii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{vanraamsdonk:LIPIcs.RTA.2013.i, author = {van Raamsdonk, Femke}, title = {{Frontmatter, Table of Contents, Preface, Conference Organization}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {i--xiii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.i}, URN = {urn:nbn:de:0030-drops-40486}, doi = {10.4230/LIPIcs.RTA.2013.i}, annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization} }
Jarkko Kari. Pattern Generation by Cellular Automata (Invited Talk). In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{kari:LIPIcs.RTA.2013.1, author = {Kari, Jarkko}, title = {{Pattern Generation by Cellular Automata}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {1--3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.1}, URN = {urn:nbn:de:0030-drops-40490}, doi = {10.4230/LIPIcs.RTA.2013.1}, annote = {Keywords: cellular automata, pattern generation, Z-numbers} }
Mitsuhiro Okada. Husserl and Hilbert on Completeness and Husserl's Term Rewrite-based Theory of Multiplicity (Invited Talk). In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 4-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{okada:LIPIcs.RTA.2013.4, author = {Okada, Mitsuhiro}, title = {{Husserl and Hilbert on Completeness and Husserl's Term Rewrite-based Theory of Multiplicity}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {4--19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.4}, URN = {urn:nbn:de:0030-drops-40524}, doi = {10.4230/LIPIcs.RTA.2013.4}, annote = {Keywords: History of term rewrite theory, Husserl, Hilbert, proof theory, Knuth-Bendix completion} }
Dimitrios Vytiniotis and Simon Peyton Jones. Evidence Normalization in System FC (Invited Talk). In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 20-38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{vytiniotis_et_al:LIPIcs.RTA.2013.20, author = {Vytiniotis, Dimitrios and Peyton Jones, Simon}, title = {{Evidence Normalization in System FC}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {20--38}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.20}, URN = {urn:nbn:de:0030-drops-40506}, doi = {10.4230/LIPIcs.RTA.2013.20}, annote = {Keywords: Haskell, type functions, system FC} }
Beniamino Accattoli. Linear Logic and Strong Normalization. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 39-54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{accattoli:LIPIcs.RTA.2013.39, author = {Accattoli, Beniamino}, title = {{Linear Logic and Strong Normalization}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {39--54}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.39}, URN = {urn:nbn:de:0030-drops-40515}, doi = {10.4230/LIPIcs.RTA.2013.39}, annote = {Keywords: linear logic, proof nets, strong normalization, explicit substitutions} }
Martin Avanzini and Georg Moser. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 55-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{avanzini_et_al:LIPIcs.RTA.2013.55, author = {Avanzini, Martin and Moser, Georg}, title = {{A Combination Framework for Complexity}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {55--70}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.55}, URN = {urn:nbn:de:0030-drops-40534}, doi = {10.4230/LIPIcs.RTA.2013.55}, annote = {Keywords: program analysis, term rewriting, complexity analysis, automation} }
Martin Avanzini and Georg Moser. Tyrolean Complexity Tool: Features and Usage. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 71-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{avanzini_et_al:LIPIcs.RTA.2013.71, author = {Avanzini, Martin and Moser, Georg}, title = {{Tyrolean Complexity Tool: Features and Usage}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {71--80}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.71}, URN = {urn:nbn:de:0030-drops-40540}, doi = {10.4230/LIPIcs.RTA.2013.71}, annote = {Keywords: program analysis, term rewriting, complexity analysis, automation} }
Kyungmin Bae, Santiago Escobar, and José Meseguer. Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 81-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{bae_et_al:LIPIcs.RTA.2013.81, author = {Bae, Kyungmin and Escobar, Santiago and Meseguer, Jos\'{e}}, title = {{Abstract Logical Model Checking of Infinite-State Systems Using Narrowing}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {81--96}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.81}, URN = {urn:nbn:de:0030-drops-40554}, doi = {10.4230/LIPIcs.RTA.2013.81}, annote = {Keywords: model checking, infinite states, rewrite theories, narrowing} }
Alexander Bau, Markus Lohrey, Eric Nöth, and Johannes Waldmann. Compression of Rewriting Systems for Termination Analysis. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 97-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{bau_et_al:LIPIcs.RTA.2013.97, author = {Bau, Alexander and Lohrey, Markus and N\"{o}th, Eric and Waldmann, Johannes}, title = {{Compression of Rewriting Systems for Termination Analysis}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {97--112}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.97}, URN = {urn:nbn:de:0030-drops-40561}, doi = {10.4230/LIPIcs.RTA.2013.97}, annote = {Keywords: termination of rewriting, matrix interpretations, constraint solving, tree compression} }
Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A Variant of Higher-Order Anti-Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 113-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{baumgartner_et_al:LIPIcs.RTA.2013.113, author = {Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu}, title = {{A Variant of Higher-Order Anti-Unification}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {113--127}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.113}, URN = {urn:nbn:de:0030-drops-40579}, doi = {10.4230/LIPIcs.RTA.2013.113}, annote = {Keywords: higher-order anti-unification, higher-order patterns} }
Yohan Boichut, Jacques Chabin, and Pierre Réty. Over-approximating Descendants by Synchronized Tree Languages. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 128-142, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{boichut_et_al:LIPIcs.RTA.2013.128, author = {Boichut, Yohan and Chabin, Jacques and R\'{e}ty, Pierre}, title = {{Over-approximating Descendants by Synchronized Tree Languages}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {128--142}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.128}, URN = {urn:nbn:de:0030-drops-40580}, doi = {10.4230/LIPIcs.RTA.2013.128}, annote = {Keywords: rewriting systems, non-regular approximations, logic programming, tree languages, descendants} }
Christophe Calvès. Unifying Nominal Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 143-157, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{calves:LIPIcs.RTA.2013.143, author = {Calv\`{e}s, Christophe}, title = {{Unifying Nominal Unification}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {143--157}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.143}, URN = {urn:nbn:de:0030-drops-40593}, doi = {10.4230/LIPIcs.RTA.2013.143}, annote = {Keywords: unification, nominal, alpha-equivalence, term-graph rewriting} }
Anupam Das. Rewriting with Linear Inferences in Propositional Logic. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 158-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{das:LIPIcs.RTA.2013.158, author = {Das, Anupam}, title = {{Rewriting with Linear Inferences in Propositional Logic}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {158--173}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.158}, URN = {urn:nbn:de:0030-drops-40609}, doi = {10.4230/LIPIcs.RTA.2013.158}, annote = {Keywords: proof theory, propositional logic, complexity of proofs, deep inference} }
Bertram Felgenhauer and Vincent van Oostrom. Proof Orders for Decreasing Diagrams. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 174-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{felgenhauer_et_al:LIPIcs.RTA.2013.174, author = {Felgenhauer, Bertram and van Oostrom, Vincent}, title = {{Proof Orders for Decreasing Diagrams}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {174--189}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.174}, URN = {urn:nbn:de:0030-drops-40616}, doi = {10.4230/LIPIcs.RTA.2013.174}, annote = {Keywords: involutive monoid, confluence modulo, decreasing diagram, proof order} }
Ken-etsu Fujita and Aleksy Schubert. Decidable structures between Church-style and Curry-style. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 190-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{fujita_et_al:LIPIcs.RTA.2013.190, author = {Fujita, Ken-etsu and Schubert, Aleksy}, title = {{Decidable structures between Church-style and Curry-style}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {190--205}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.190}, URN = {urn:nbn:de:0030-drops-40629}, doi = {10.4230/LIPIcs.RTA.2013.190}, annote = {Keywords: 2nd-order lambda-calculus, type-checking, type-inference, Church-style and Curry-style} }
Clemens Grabmayer and Jan Rochel. Expressibility in the Lambda Calculus with Mu. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 206-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{grabmayer_et_al:LIPIcs.RTA.2013.206, author = {Grabmayer, Clemens and Rochel, Jan}, title = {{Expressibility in the Lambda Calculus with Mu}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {206--222}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.206}, URN = {urn:nbn:de:0030-drops-40635}, doi = {10.4230/LIPIcs.RTA.2013.206}, annote = {Keywords: lambda-calculus, lambda-calculus with letrec, unfolding semantics, regularity for infinite lambda-terms, binding-capturing chain} }
Yves Guiraud, Philippe Malbos, and Samuel Mimram. A Homotopical Completion Procedure with Applications to Coherence of Monoids. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 223-238, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{guiraud_et_al:LIPIcs.RTA.2013.223, author = {Guiraud, Yves and Malbos, Philippe and Mimram, Samuel}, title = {{A Homotopical Completion Procedure with Applications to Coherence of Monoids}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {223--238}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.223}, URN = {urn:nbn:de:0030-drops-40649}, doi = {10.4230/LIPIcs.RTA.2013.223}, annote = {Keywords: higher-dimensional rewriting, presentation of monoid, Knuth-Bendix completion, Tietze transformation, low-dimensional homotopy for monoids, coherence} }
Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 239-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.239, author = {Schmidt-Schau{\ss}, Manfred and Machkasova, Elena and Sabel, David}, title = {{Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {239--254}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.239}, URN = {urn:nbn:de:0030-drops-40651}, doi = {10.4230/LIPIcs.RTA.2013.239}, annote = {Keywords: lazy lambda calculus, contextual semantics, conservativity} }
Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 255-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.255, author = {Schmidt-Schau{\ss}, Manfred and Rau, Conrad and Sabel, David}, title = {{Algorithms for Extended Alpha-Equivalence and Complexity}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {255--270}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.255}, URN = {urn:nbn:de:0030-drops-40667}, doi = {10.4230/LIPIcs.RTA.2013.255}, annote = {Keywords: alpha-equivalence, higher-order calculi, deduction, pi-calculus} }
Gert Smolka and Tobias Tebbi. Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 271-286, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{smolka_et_al:LIPIcs.RTA.2013.271, author = {Smolka, Gert and Tebbi, Tobias}, title = {{Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {271--286}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.271}, URN = {urn:nbn:de:0030-drops-40674}, doi = {10.4230/LIPIcs.RTA.2013.271}, annote = {Keywords: recursion schemes, semi-unification, infinitary rewriting} }
Christian Sternagel and René Thiemann. Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 287-302, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{sternagel_et_al:LIPIcs.RTA.2013.287, author = {Sternagel, Christian and Thiemann, Ren\'{e}}, title = {{Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {287--302}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.287}, URN = {urn:nbn:de:0030-drops-40685}, doi = {10.4230/LIPIcs.RTA.2013.287}, annote = {Keywords: certification, completion, confluence, termination} }
Elena Tushkanova, Christophe Ringeissen, Alain Giorgetti, and Olga Kouchnarenko. Automatic Decidability: A Schematic Calculus for Theories with Counting Operators. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 303-318, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{tushkanova_et_al:LIPIcs.RTA.2013.303, author = {Tushkanova, Elena and Ringeissen, Christophe and Giorgetti, Alain and Kouchnarenko, Olga}, title = {{Automatic Decidability: A Schematic Calculus for Theories with Counting Operators}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {303--318}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.303}, URN = {urn:nbn:de:0030-drops-40696}, doi = {10.4230/LIPIcs.RTA.2013.303}, annote = {Keywords: decision procedures, superposition, schematic saturation} }
Sarah Winkler and Aart Middeldorp. Normalized Completion Revisited. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 319-334, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{winkler_et_al:LIPIcs.RTA.2013.319, author = {Winkler, Sarah and Middeldorp, Aart}, title = {{Normalized Completion Revisited}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {319--334}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.319}, URN = {urn:nbn:de:0030-drops-40702}, doi = {10.4230/LIPIcs.RTA.2013.319}, annote = {Keywords: term rewriting, completion} }
Sarah Winkler, Harald Zankl, and Aart Middeldorp. Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 335-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{winkler_et_al:LIPIcs.RTA.2013.335, author = {Winkler, Sarah and Zankl, Harald and Middeldorp, Aart}, title = {{Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {335--351}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.335}, URN = {urn:nbn:de:0030-drops-40718}, doi = {10.4230/LIPIcs.RTA.2013.335}, annote = {Keywords: term rewriting, termination, automation, ordinals} }
Harald Zankl. Confluence by Decreasing Diagrams – Formalized. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 352-367, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{zankl:LIPIcs.RTA.2013.352, author = {Zankl, Harald}, title = {{Confluence by Decreasing Diagrams – Formalized}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {352--367}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.352}, URN = {urn:nbn:de:0030-drops-40723}, doi = {10.4230/LIPIcs.RTA.2013.352}, annote = {Keywords: term rewriting, confluence, decreasing diagrams, formalization} }
Feedback for Dagstuhl Publishing