Related Research Articles
In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution.
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
Hendrik Pieter (Henk) Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.
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.
David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.
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 Conference on Artificial General Intelligence is a meeting of researchers in the field of Artificial General Intelligence organized by the AGI Society and held annually since 2008. The conference was initiated by the 2006 Bethesda Artificial General Intelligence Workshop and has been hosted at the University of Memphis ; Arlington, Virginia ; Lugano, Switzerland ; Google headquarters in Mountain View, California ; the University of Oxford, United Kingdom ; and at Peking University, Beijing, China, Quebec City, Canada. The AGI-15 conference was held in Berlin, Germany.
A term graph is a representation of an expression in a formal language as a generalized graph whose vertices are terms. Term graphs are a more powerful form of representation than expression trees because they can represent not only common subexpressions but also cyclic/recursive subexpressions.
Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.
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.
In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment, or encompassment, preorder (≤) on the set of terms, is defined by
In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have turned out to be useful in theoretical investigations.
Bruno Courcelle is a French mathematician and computer scientist, best known for Courcelle's theorem in graph theory.
In mathematics and theoretical computer science, a set constraint is an equation or an inequation between sets of terms. Similar to systems of (in)equations between numbers, methods are studied for solving systems of set constraints. Different approaches admit different operators on sets and different (in)equation relations between set expressions.
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.
A downgrade attack, also called a bidding-down attack, or version rollback attack, is a form of cryptographic attack on a computer system or communications protocol that makes it abandon a high-quality mode of operation in favor of an older, lower-quality mode of operation that is typically provided for backward compatibility with older systems. An example of such a flaw was found in OpenSSL that allowed the attacker to negotiate the use of a lower version of TLS between the client and server. This is one of the most common types of downgrade attacks. Opportunistic encryption protocols such as STARTTLS are generally vulnerable to downgrade attacks, as they, by design, fall back to unencrypted communication. Websites which rely on redirects from unencrypted HTTP to encrypted HTTPS can also be vulnerable to downgrade attacks, as the initial redirect is not protected by encryption.
References
- ↑ Curriculum vitae
- ↑ Marc Bezem; Jan Willem Klop; Roel de Vrijer, eds. (2003). Terese — Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Vol. 55. Cambridge: Cambridge University Press.
- ↑ Jan Willem Klop (2007). "New Fixed Point Combinators From Old" (PDF). In Erik Barendsen; Herman Geuvers; Venanzio Capretta; Milad Niqui (eds.). Reflections on Type Theory, Lambda Calculus, and the Mind — Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday]. University Nijmegen. pp. 197–210. ISBN 978-90-9022446-6. Here: nr.1.3, p.198
- ↑ "Jan Willem Klop". Royal Netherlands Academy of Arts and Sciences. Archived from the original on 8 February 2016. Retrieved 8 February 2016.
