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).
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.
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.
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.
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.
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.
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.
