International Conference on Rewriting Techniques and Applications

Last updated

Rewriting Techniques and Applications (RTA) is an annual international academic conference on the topic of rewriting. It covers all aspects of rewriting, including termination, equational reasoning, theorem proving, higher-order rewriting, unification and the lambda calculus. The conference consists of peer-reviewed papers with the proceedings published by Springer in the LNCS series until 2009, and since then in the LIPIcs series published by the Leibniz-Zentrum für Informatik. Several rewriting-related workshops are also affiliated with RTA.

The first RTA was held in Dijon, France in September 1983. RTA took part in the federated conferences Federated Logic Conference (FLoC) and Rewriting, Deduction, and Programming (RDP). In 2016, RTA merged with the International Conference on Typed Lambda Calculi and Applications to form the International Conference on Formal Structures for Computation and Deduction (FSCD).


Related Research Articles

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

The Larch Prover, or LP for short, was an interactive theorem proving system for multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990s to reason about designs for circuits, concurrent algorithms, hardware, and software.

<span class="mw-page-title-main">Henk Barendregt</span> Dutch logician (born 1947)

Hendrik Pieter (Henk) Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

<span class="mw-page-title-main">Programming language theory</span> Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.

Gérard Pierre Huet is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and to the theory of computation.

The International Workshop on First-Order Theorem Proving (FTP) is a scientific meeting of researchers interested in automated theorem proving for first-order logic and related fields. FTP workshops are less formal than many conferences, but more formal than most workshops. While FTP proceedings are published informally, most FTP workshops have resulted in a special issue of a recognized peer-reviewed academic journal.

Nominal terms are a metalanguage for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence. Nominal terms came out of a programme of research into nominal sets, and have a concrete semantics in those sets.

Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of TeReSe and his fixed point combinator

Anti-unification is the process of constructing a generalization common to two given symbolic expressions. As in unification, several frameworks are distinguished depending on which expressions are allowed, and which expressions are considered equal. If variables representing functions are allowed in an expression, the process is called "higher-order anti-unification", otherwise "first-order anti-unification". If the generalization is required to have an instance literally equal to each input expression, the process is called "syntactical anti-unification", otherwise "E-anti-unification", or "anti-unification modulo theory".

In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.

<span class="mw-page-title-main">Vienna Summer of Logic</span> Scientific event

The Vienna Summer of Logic was a scientific event in the summer of 2014, combining 12 major conferences and several workshops from the fields of mathematical logic, logic in computer science, and logic in artificial intelligence. The meetings took place from July 9 to 24, 2014, and attracted more than 2000 scientists and researchers.

<span class="mw-page-title-main">Jean-Pierre Jouannaud</span> French computer scientist (born 1947)

Jean-Pierre Jouannaud is a French computer scientist, known for his work in the area of term rewriting.

Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.

Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory.

Tobias Nipkow is a German computer scientist.

Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.