yusuke1997/dblp-id-title huggingface dataset:
Term Rewriting and Universal Algebra in Historical Perspective (Abstract of Invited Lecture)
Th Word Problem for Finitely Presented Monoids and Finite Canonical Rewriting Systems
Usable Rules for Context-Sensitive Rewrite Systems
Automatic Monoids Versus Monoids with Finite Convergent Presentations
Two Results in Term Rewriting Theorem Proving
Static Analysis of Modularity of beta-Reduction in the Hyperbalanced lambda-Calculus
Superposition Theorem Proving for Albelian Groups Represented as Integer Modules
Root-Labeling
Relating Accumulative and Non-accumulative Functional Programs
Combining Equational Tree Automata over AC and ACI Theories
Rewriting with Linear Inferences in Propositional Logic
A Restricted Form on Higher-Order Rewriting Applied to an HDL Semantics
Encompassment Properties and Automata with Constraints
Matching Power
FAST: An Efficient Decision Procedure for Deduction and Static Equivalence
Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
Rewriting Modulo in Deduction Modulo
Unions of Equational Monadic Theories
Well-Definedness of Streams by Termination
DISCOUNT: A SYstem for Distributed Equational Deduction
Transforming Context-Sensitive Rewrite Systems
Confluence and Termination of Simply Typed Term Rewriting Systems
Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification
Rewriting Techniques and Applications, 13th International Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings
Confluence of an Extension of Combinatory Logic by Boolean Constants
Generalized Innermost Rewriting
Axiomatic Sharing-via-Labelling
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
A Characterisation of Multiply Recursive Functions with Higman's Lemma
Rewriting, and Equational Unification: the Higher-Order Cases
Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms
Groups Presented by Certain Classes of Finite Length-Reducing String-Rewriting Systems
DynSem: A DSL for Dynamic Semantics Specification
LAMBDALG: Higher Order Algebraic Specification Language
Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings
Query Optimization Using Rewrite Rules
Universal Algebra for Termination of Higher-Order Rewriting
Topics in Termination
Models of Type Theory Based on Moore Paths
Some Results about Confluence on a Given Congruence Class
Proving Properties of Term Rewrite Systems via Logic Programs
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Natural Inductive Theorems for Higher-Order Rewriting
Confluence of Pattern-Based Calculi
Focusing in Orthologic
Dismatching and Local Disunification in EL
On the Strong Normalisation of Natural Deduction with Permutation-Conversions
Inductive Proofs by Specification Transformation
Adjunction for Garbage Collection with Application to Graph Rewriting
Realising Optimal Sharing
On Fairness of Completion-Based Theorem Proving Strategies
Formal Verification of an Optimizing Compiler
The Joinability and Unification Problems for Confluent Semi-constructor TRSs
Higher-Order Equational Pattern Anti-Unification
Cumulative Inductive Types In Coq
Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient parallel Execution
TORPA: Termination of Rewriting Proved Automatically
Dependency Pairs for Simply Typed Term Rewriting
A Simple and Efficient Step Towards Type-Correct XSLT Transformations
A Verification Technique Using Term Rewriting Systems and Abstract Interpretation
Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear lambda -Calculus
Combination Techniques and Decision Problems for Disunification
Regular Sets of Descendants by Some Rewrite Strategies
Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus
On Relationship Between Term Rewriting Systems and Regular Tree Languages
Complexity of Matching Problems
Arctic Termination ...Below Zero
Termination Proofs and the Length of Derivations (Preliminary Version)
Anti-Unification: Algorithms and Applications
Proving Properties of Typed Lambda Terms: Realizability, Covers, and Sheaves (Abstract)
Reinterpreting Compression in Infinitary Rewriting
Consider Only General Superpositions in Completion Procedures
ANIGRAF: An Interactive System for the Animation of Graph Rewriting Systems with Priorities
Narrowing Directed by a Graph of Terms
Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
Infinitary Combinatory Reduction Systems
Any Gound Associative-Commutative Theory Has a Finite Canonical System
A Path Order for Rewrite Systems that Compute Exponential Time Functions
Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings
Applications of Rewrite Techniques in Monoids and Rings (Abstract)
Challenges in Satisfiability Modulo Theories
Tom: Piggybacking Rewriting on Java
Rewriting Techniques and Applications, 5th International Conference, RTA-93, Montreal, Canada, June 16-18, 1993, Proceedings
Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings
XML Schema, Tree Logic and Sheaves Automata
Tyrolean Complexity Tool: Features and Usage
A Variant of Higher-Order Anti-Unification
Improving Rewriting Induction Approach for Proving Ground Confluence
Automata for Data Words and Data Trees
On Dinaturality, Typability and beta-eta-Stable Models
EMMY: A Refutational Theorem Prover for First-Order Logic with Equation
Functional-Logic Graph Parser Combinators
Well-Behaved Search and the Robbins Problem
Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover
Category Theory in Coq 8.5
The Calculus of algebraic Constructions
Priority Rewriting: Semantics, Confluence, and Conditional
Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete
Paths, Computations and Labels in the Lambda-Calculus
Weak Convergence and Uniform Normalization in Infinitary Rewriting
Incremental Techniques for Efficient Normalization of Nonlinear Rewrite Systems
Globular: An Online Proof Assistant for Higher-Dimensional Rewriting
A Diagrammatic Axiomatisation of Fermionic Quantum Circuits
Abstract Critical Pairs and Confluence of Arbitrary Binary Relations
Termination Analysis of C Programs Using Compiler Intermediate Languages
Rewrite Games
AC Unification Through Order-Sorted AC1 Unification
Meaningless Sets in Infinitary Combinatory Logic
Transfinite Reductions in Orthogonal Term Rewriting Systems (Extended Abstract)
Axiomatic Rewriting Theory VI Residual Theory Revisited
A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property
Pattern Generation by Cellular Automata (Invited Talk)
A Compiler for Nondeterministic Term Rewriting Systems
Ground Confluence
The Set of Unifiers in Typed Lambda-Calculus as Regular Expression
Rewriting Logic and Maude: Concepts and Applications
HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell (Invited Talk)
Automatic Decidability: A Schematic Calculus for Theories with Counting Operators
Weakly Regular Relations and Applications
Conditional Complexity
Confluent Term Rewriting Systems
Nominal Anti-Unification
Associative-Commutative Rewriting on Large Terms
A Polynomial Algorithm Testing Partial Confluence of Basic Semi-Thue Systems
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving
Explicit Substitutions with de Bruijn's Levels
Homological Computations for Term Rewriting Systems
Strategic Pattern Matching
Extension of the Associative Path Ordering to a Chain of Associative Commutative Symbols
Presenting a Category Modulo a Rewriting System
The Independence of Markov's Principle in Type Theory
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
Deriving an Abstract Machine for Strong Call by Need
Tyrolean Termination Tool 2
Diagram Rewriting for Orthogonal Matrices: A Study of Critical Peaks
An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation
Higher-Order Superposition for Dependent Types
Abstract Rewriting with Concrete Operations
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning
Sequence Unification Through Currying
Left-to-Right Tree Pattern Matching
Complete Sets of Reductions Modulo Associativity, Commutativity and Identity
Infinitary Term Graph Rewriting is Simple, Sound and Complete
PETRIREVE: Proving Petri Net Properties with Rewriting Systems
Rewriting Models of Boolean Programs
The Termination Competition
SN Combinators and Partial Combinatory Algebras
An Extensional Böhm Model
mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting
Tree Automata and Term Rewrite Systems
Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2
Proof Nets for First-Order Additive Linear Logic
LEMMA: A System for Automated Synthesis of Recursive Programs in Equational Theories
Solving Partial Order Constraints for LPO Termination
E -Unification for Subsystems of S4
Combining Pattern E-Unification Algorithms
Linear Higher-Order Matching Is NP-Complete
Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
Termination by Quasi-periodic Interpretations
Types as Resources for Classical Natural Deduction
Bicategories in Univalent Foundations
The Maude 2.0 System
Normalisation by Evaluation for Dependent Types
Beta Reduction Constraints
Termination of String Rewriting with Matrix Interpretations
Environments for Term Rewriting Engines for Free!
A Visual Environment for Developing Context-Sensitive Term Rewriting Systems
Implicational Relevance Logic is 2-ExpTime-Complete
The Delta-calculus: Syntax and Types
Maximal Completion
Unification and Anti-unification modulo Equational Theories
Invited Talk: Symbolic Systems Biology
Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
A New Proof Manager and Graphic Interface for Larch Prover
Termination of Single-Threaded One-Rule Semi-Thue Systems
Testing Extended Regular Language Membership Incrementally by Rewriting
Classes of Equational Programs that Compile into Efficient Machine Code
The Derivational Complexity Induced by the Dependency Pair Method
Simulation in the Call-by-Need Lambda-Calculus with letrec
A Fresh Look at the lambda-Calculus (Invited Talk)
Dependency Pairs and Polynomial Path Orders
Symideal Gröbner Bases
Optimizing Equational Programs
Process Types as a Descriptive Tool for Interaction - Control and the Pi-Calculus
Completeness of Combinations of Constructor Systems
Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data
About Proofs by Consistency (Abstract)
Embedding with Patterns and Associated Recursive Path Ordering
An Efficient Nominal Unification Algorithm
Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems
Universal Interaction Systems with Only Two Agents
UNIMOK: A System for Combining Equational Unification Algorithm
Exceptions in the Rewriting Calculus
Deciding the Word Problem in the Union of Equational Theories Sharing Constructors
Proving Confluence of Term Rewriting Systems Automatically
Expressibility in the Lambda Calculus with Mu
Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic
Finite Family Developments
Coherence of Gray Categories via Rewriting
Determining Unify-Stable Presentations
Hybrid Unification in the Description Logic EL
Combining Unification Algorithms for Confined Regular Equational Theories
1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, June 22-26, 2016
Stable Computational Semantics of Conflict-Free Rewrite Systems (Partial Orders with Duplication)
Simulation Buchberger's Algorithm by Knuth-Bendix Completion
Negative Translations and Normal Modality
Equational and Membership Constraints for Finite Trees
Proof-Producing Congruence Closure
KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis
On the Termination Problem for One-Rule Semi-Thue System
Labelings for Decreasing Diagrams
Modular Complexity Analysis via Relative Complexity
Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee
A Rewriting Logic Semantics Approach to Modular Program Analysis
Leanest Quasi-orderings
Comparing Böhm-Like Trees
Polynomial Interpretations for Higher-Order Rewriting
A Compiler for Conditional Term Rewriting Systems
Combining Matching Algorithms: The Rectangular Case
3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, Oxford, UK, July 9-12, 2018
Monotonic AC-Compatible Semantic Path Orderings
Proving Quadratic Derivational Complexities Using Context Dependent Interpretations
No complete linear term rewriting system for propositional logic
Coalgebras and Higher-Order Computation: a GoI Approach
Efficient lambda-Evaluation with Interaction Nets
Dependency Pairs Revisited
Cut Admissibility by Saturation
Preciseness of Subtyping on Intersection and Union Types
Orderings for Innermost Termination
First-Order Formative Rules
Fast Many-to-One Matching Algorithms
Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding
Optimality and the Linear Substitution Calculus
Decidability for Left-Linaer Growing Term Rewriting Systems
Termination Analysis of the Untyped lamba-Calculus
Rule-Based Analysis of Dimensional Safety
Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems
D-Bases for Polynomial Ideals over Commutative Noetherian Rings
Uniform Normalisation beyond Orthogonality
Querying Unranked Trees with Stepwise Tree Automata
Quasi-interpretations and Small Space Bounds
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
Multiset Rewriting and Security Protocol Analysis
The Unification Problem for Confluent Right-Ground Term Rewriting Systems
Generalized Gröbner Bases: Theory and Applications. A Condensation
An Equational Logic Sampler
Turing-Completeness of Polymorphic Stream Equation Systems
On Ground AC-Completion
Negation with Logical Variables in Conditional Rewriting
EPIC: An Equational Language -Abstract Machine Supporting Tools-
Linear Second-Order Unification
Termination Transformation by Tree Lifting Ordering
Normalization via Rewrite Closures
On the Connections between Rewriting and Formal Language Theory
Index-Stratified Types
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, Novi Sad, Serbia, May 30 - June 1, 2011
Fixed-Point Constraints for Nominal Equational Unification
Matchbox: A Tool for Match-Bounded String Rewriting
A Sufficient Completeness Reasoning Tool for Partial Specifications
Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings
Nominal Unification with Atom and Context Variables
Termination of String Rewriting Rules That Have One Pair of Overlaps
Unification and Logarithmic Space
Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides
The Invariant Package of MAS
Decidable Approximations of Term Rewriting Systems
A Proof Calculus Which Reduces Syntactic Bureaucracy
Termination of linear bounded term rewriting systems
Proving Equality of Streams Automatically
Böhm-Like Trees for Term Rewriting Systems
Counting Environments and Closures
Problems in Rewriting Applied to Categorical Concepts by the Example of a Computational Comonad
Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization
Böhm Reduction in Infinitary Term Graph Rewriting Systems
Solved Forms for Path Ordering Constraints
Declarative Debugging of Missing Answers for Maude
Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language
The Algebra of Equality Proofs
STORM: A MAny-to-One Associative-Commutative Matcher
On How To Move Mountains 'Associatively and Commutatively'
Total Termination of Term Rewriting
Solving Type Equations by Graph Rewriting
The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus
Divergence Phenomena during Completion
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
Towards a Domain Theory for Termination Proofs
Ramsey Theorem as an Intuitionistic Property of Well Founded Relations
On Normalisation of Infinitary Combinatory Reduction Systems
Redex Capturing in Term Graph Rewriting (Concise Version)
Rewriting UNITY
Normalisation in Weakly Orthogonal Rewriting
Two-Way Equational Tree Automata for AC-Like Theories: Decidability and Closure Properties
A Needed Rewriting Strategy for Data-Structures with Pointers
4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany, June 24-30, 2019
Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings
Detecting Redundant Narrowing Derivations by the LSE-SL Reducability Test
Classical Extraction in Continuation Models
Weighted Relational Models for Mobility
New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable
Expression Reduction Systems with Patterns
Unification and Matching in Process Algebras
A Rewrite Mechanism for Logic Programs with Negation
A Complete Axiomatisation for the Inclusion of Series-Parallel Partial Orders
Simulation of Turning Machines by a Left-Linear Rewrite Rule
The Existential Fragment of the One-Step Parallel Rewriting Theory
SbReve2: A Term Rewriting Laboratory with (AC-) Unfailing Completion
A Fibrational Framework for Substructural and Modal Logics
Proving the Genericity Lemma by Leftmost Reduction is Simple
The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic
A Rule-Based Approach for Automated Generation of Kinetic Chemical Mechanisms
Call-by-Value Is Dual to Call-by-Name - Reloaded
Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)
How to Choose Weights in the Knuth Bendix Ordering
Termination of (Canonical) Context-Sensitive Rewriting
Local States in String Diagrams
Graph Grammars, A New Paradigma for Implementing Visual Languages
Propositional Tree Automata
Evidence Normalization in System FC (Invited Talk)
Recursive Derivational Length Bounds for Confluent Term Rewrite Systems
On Repetitive Right Application of B-Terms
Some Lambda Calculi with Categorial Sums and Products
Formal Languages, Formally and Coinductively
Handling Function Definitions through Innermost Superposition and Rewriting
There Is Only One Notion of Differentiation
Context-Sensitive AC-Rewriting
Call-by-Name Gradual Type Theory
Modes of Convergence for Term Graph Rewriting
An Explicit Framework for Interaction Nets
Semantics and Strong Sequentiality of Priority Term Rewriting Systems
Normal Forms and Reduction for Theories of Binary Relations
Modular Termination of Basic Narrowing
Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings
Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings
From Outermost to Context-Sensitive Rewriting
Complexity Hierarchies and Higher-Order Cons-Free Rewriting
(Head-) Normalization of Typeable Rewrite Systems
A Term Rewriting System for Kuratowski's Closure-Complement Problem
Residuals in Higher-Order Rewriting
Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk)
Extensions and Comparison of Simplification Orderings
Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk)
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
Arrays and References in Resource Aware ML
A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case
Near Semi-rings and Lambda Calculus
Restrictions of Congruence Generated by Finite Canonical String-Rewriting Systems
Termination Proofs by Context-Dependent Interpretations
Cross-Sections for Finitely Presented Monoids with Decidable Word Problems
JITty: A Rewriter with Strategy Annotations
AGG - An Implementation of Algebraic Graph Rewriting
Modularity of Completeness Revisited
An Algebra of Resolution
Functions-as-Constructors Higher-Order Unification
On the Parallel Complexity of Tree Automata
A Combination Framework for Complexity
The Equivalence of Boundary and Confluent Graph Grammars on Graph Languages of Bounded Degree
The Decidability of Simultaneous Rigid E -Unification with One Variable
Proving Termination of Rewrite Systems Using Bounds
Husserl and Hilbert on Completeness and Husserl's Term Rewrite-based Theory of Multiplicity (Invited Talk)
The First-Order Theory of One-Step Rewriting is Undecidable
Sparse Tiling Through Overlap Closures for Termination of String Rewriting
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
Challenges in Quantum Programming Languages (Invited Talk)
The Complexity of Principal Inhabitation
Tsukuba Termination Tool
Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings
A Rewriting Alternative to Reidemeister-Schreier
Arithmetic as a Theory Modulo
Rewriting Techniques for Program Synthesis
Test Sets for the Universal and Existential Closure of Regular Tree Languages
Modal Embeddings and Calling Paradigms
A Complete Characterization of Termination of O p 1 q -> 1 r O s
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Automata and Logics for Unranked and Unordered Trees
Modularity of Termination in Term Graph Rewriting
An Efficient Representation of Arithmetic for Term Rewriting
Triangulation in Rewriting
Amortised Resource Analysis and Typed Polynomial Interpretations
Term-Graph Rewriting Via Explicit Paths
Certified Subterm Criterion and Certified Usable Rules
Thue Systems as Rewriting Systems
Formalizing Bialgebraic Semantics in PVS 6.0
All-Path Reachability Logic
AC-Complete Unification and its Application to Theorem Proving
TALP: A Tool for the Termination Analysis of Logic Programs
Rewriting Strategies for Instruction Selection
Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories
Tree Automata with Height Constraints between Brothers
Validation of the JavaCard Platform with Implicit Induction Techniques
The Finite Variant Property: How to Get Rid of Some Algebraic Properties
On Some Mathematical Logic Contributions to Rewriting Techniques: Lost Heritage (Abstract)
Confluence as a Cut Elimination Property
Checking Conservativity of Overloaded Definitions in Higher-Order Logic
Coupling Saturation-Based Provers by Exchanging Positive/Negative Information
Optimization by Non-Deterministic, Lazy Rewriting
A Graph Reduction Approach to Incremental Term Rewriting (Preliminary Report)
Linear-algebraic lambda-calculus: higher-order, encodings, and confluence.
On Equational Theories, Unification and Decidability
An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting
Proof Nets for Bi-Intuitionistic Linear Logic
Confluence of Prefix-Constrained Rewrite Systems
A Normal Form for Church-Rosser Language Systems
Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings
Algorithms for Extended Alpha-Equivalence and Complexity
Tradeoffs in the Intensional Representation of Lambda Terms
Proving Termination of Integer Term Rewriting
A Proof Theoretic Analysis of Intruder Theories
A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code
Effective Reduction and Conversion Strategies for Combinators
Regular Substitution Sets: A Means of Controlling E-Unification
A Precedence-Based Total AC-Compatible Ordering
Completion for Logically Constrained Rewriting