Computability theory

Summary

Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since expanded to include the study of generalized computability and definability. In these areas, computability theory overlaps with proof theory and effective descriptive set theory. Basic questions addressed by computability theory include:

What does it mean for a function on the natural numbers to be computable?
How can noncomputable functions be classified into a hierarchy based on their level of noncomputability?

Although there is considerable overlap in terms of knowledge and methods, mathematical computability theorists study the theory of relative computability, reducibility notions, and degree structures; those in the computer science field focus on the theory of subrecursive hierarchies, formal methods, and formal languages. Intr

Official source

https://en.wikipedia.org/wiki/Computability_theory

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (5)

Related publications

Related people

Related units

Related concepts (50)

Related concepts

Related courses (15)

Related courses

Related lectures (15)

Related lectures

New Directions in Cryptanalysis of Self-Synchronizing Stream Ciphers

Shahram Khazaei, Willi Meier

In cryptology we commonly face the problem of finding an unknown key K from the output of an easily computable keyed function F(C, K) where the attacker has the power to choose the public variable C. In this work we focus on self-synchronizing stream ciphers. First we show how to model these primitives in the above-mentioned general problem by relating appropriate functions F to the underlying ciphers. Then we apply the recently proposed framework presented at AfricaCrypt'08 by Fischer et. al. for dealing with this kind of problems to the proposed T-function based self-synchronizing stream cipher by Klimov and Shamir at FSE'05 and show how to deduce some non-trivial information about the key. We also open a new window for answering a crucial question raised by Fischer et. al. regarding the problem of finding weak IV bits which is essential for their attack.

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2008

Motivated by the advantages of using elliptic curves for discrete logarithm-based public-key cryptography, there is an active research area investigating the potential of using hyperelliptic curves of genus 2. For both types of curves, the best known algorithms to solve the discrete logarithm problem are generic attacks such as Pollard rho, for which it is well-known that the algorithm can be sped up when the target curve comes equipped with an efficiently computable automorphism. In this paper we incorporate all of the known optimizations (including those relating to the automorphism group) in order to perform a systematic security assessment of two elliptic curves and two hyperelliptic curves of genus 2. We use our software framework to give concrete estimates on the number of core years required to solve the discrete logarithm problem on four curves that target the 128-bit security level: on the standardized NIST CurveP-256, on a popular curve from the Barreto-Naehrig family, and on their respective analogues in genus 2. © 2014 Springer-Verlag Berlin Heidelberg.

Springer Berlin Heidelberg2014

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux calculus for that fragment which uses as oracles a decision procedure for linear integer arithmetic and a number of computable functions over regular expressions. A distinguishing feature of this calculus is that it provides a completely algebraic method for solving membership constraints which can be easily integrated into multi-theory SMT solvers. Another is that it can be used to generate symbolic solutions for such constraints, that is, solved forms that provide simple and compact representations of entire sets of complete solutions. The calculus is part of a larger one providing the theoretical foundations of a high performance theory solver for string constraints implemented in the SMT solver CVC4.

Springer-Verlag Berlin2015