Faster access than browser!
122 relations: Abstract machine, Academic Press, Algebraic data type, Analogy, Andrey Kolmogorov, Apply, Arend Heyting, Automath, Axiom of choice, Axiom schema, Bottom type, Brouwer–Heyting–Kolmogorov interpretation, Calculus of constructions, Calculus of structures, Call-with-current-continuation, Cartesian closed category, Categorical logic, Category theory, Classical logic, Closed monoidal category, Cobordism, Combinatory logic, Computer program, Conditional proof, Continuation, Continuation-passing style, Coq, Corecursion, Correctness (computer science), Currying, Dag Prawitz, Data type, Deduction theorem, Dependent type, Dialectica interpretation, Double-negation translation, Elsevier, Evaluation strategy, Existential quantification, Formal system, Function type, Functional programming, Genetic programming, Georg Kreisel, Gerhard Gentzen, Grothendieck topology, Haskell Curry, Higher-order logic, Hilbert system, Homotopy, ..., Homotopy type theory, Hypothesis, Initial and terminal objects, Institute for Advanced Study, Intuitionism, Intuitionistic logic, Intuitionistic type theory, Joachim Lambek, Kurt Gödel, L. E. J. Brouwer, Lambda calculus, Lambda-mu calculus, Linear logic, Logic, Logic for Programming, Artificial Intelligence and Reasoning, Logic programming, Logical conjunction, Logical consequence, Logical disjunction, Mathematical induction, Mathematical proof, Mathematician, Modal logic, Model of computation, Modus ponens, Monad (functional programming), Natural deduction, Nicolaas Govert de Bruijn, Normalization property (abstract rewriting), Oxford University Press, Peirce's law, Per Martin-Löf, Peter Johnstone (mathematician), Principal type, Product type, Programming language, Programming language theory, Proof calculus, Proof net, Proof theory, Proof-carrying code, Realizability, Recursion (computer science), Relevance logic, Return type, Rule of inference, Sequent, Sequent calculus, Set theory, Simply typed lambda calculus, Springer Science+Business Media, Stephen Cole Kleene, String theory, Substructural type system, System F, Tagged union, Tautology (logic), Thierry Coquand, Total functional programming, Turing completeness, Turing machine, Type inhabitation, Type rule, Type system, Type theory, Typed assembly language, Typed lambda calculus, Unifying theories in mathematics, Unit type, Universal quantification, Well-formed formula, William Alvin Howard. Expand index (72 more) »
Abstract machine
An abstract machine, also called an abstract computer, is a theoretical model of a computer hardware or software system used in automata theory.
New!!: Curry–Howard correspondence and Abstract machine · See more »
Academic Press
Academic Press is an academic book publisher.
New!!: Curry–Howard correspondence and Academic Press · See more »
Algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.
New!!: Curry–Howard correspondence and Algebraic data type · See more »
Analogy
Analogy (from Greek ἀναλογία, analogia, "proportion", from ana- "upon, according to" + logos "ratio") is a cognitive process of transferring information or meaning from a particular subject (the analog, or source) to another (the target), or a linguistic expression corresponding to such a process.
New!!: Curry–Howard correspondence and Analogy · See more »
Andrey Kolmogorov
Andrey Nikolaevich Kolmogorov (a, 25 April 1903 – 20 October 1987) was a 20th-century Soviet mathematician who made significant contributions to the mathematics of probability theory, topology, intuitionistic logic, turbulence, classical mechanics, algorithmic information theory and computational complexity.
New!!: Curry–Howard correspondence and Andrey Kolmogorov · See more »
Apply
In mathematics and computer science, apply is a function that applies functions to arguments.
New!!: Curry–Howard correspondence and Apply · See more »
Arend Heyting
__notoc__ Arend Heyting (9 May 1898 – 9 July 1980) was a Dutch mathematician and logician.
New!!: Curry–Howard correspondence and Arend Heyting · See more »
Automath
Automath ("automating mathematics") was a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.
New!!: Curry–Howard correspondence and Automath · See more »
Axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that the Cartesian product of a collection of non-empty sets is non-empty.
New!!: Curry–Howard correspondence and Axiom of choice · See more »
Axiom schema
In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
New!!: Curry–Howard correspondence and Axiom schema · See more »
Bottom type
In type theory, a theory within mathematical logic, the bottom type is the type that has no values.
New!!: Curry–Howard correspondence and Bottom type · See more »
Brouwer–Heyting–Kolmogorov interpretation
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov.
New!!: Curry–Howard correspondence and Brouwer–Heyting–Kolmogorov interpretation · See more »
Calculus of constructions
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand.
New!!: Curry–Howard correspondence and Calculus of constructions · See more »
Calculus of structures
The calculus of structures is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic.
New!!: Curry–Howard correspondence and Calculus of structures · See more »
Call-with-current-continuation
In Scheme programming, the function call-with-current-continuation, abbreviated call/cc, is used as a control operator.
New!!: Curry–Howard correspondence and Call-with-current-continuation · See more »
Cartesian closed category
In category theory, a category is considered Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors.
New!!: Curry–Howard correspondence and Cartesian closed category · See more »
Categorical logic
Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic.
New!!: Curry–Howard correspondence and Categorical logic · See more »
Category theory
Category theory formalizes mathematical structure and its concepts in terms of a labeled directed graph called a category, whose nodes are called objects, and whose labelled directed edges are called arrows (or morphisms).
New!!: Curry–Howard correspondence and Category theory · See more »
Classical logic
Classical logic (or standard logic) is an intensively studied and widely used class of formal logics.
New!!: Curry–Howard correspondence and Classical logic · See more »
Closed monoidal category
In mathematics, especially in category theory, a closed monoidal category (or a monoidal closed category) is a category which is both a monoidal category and a closed category in such a way that the structures are compatible.
New!!: Curry–Howard correspondence and Closed monoidal category · See more »
Cobordism
In mathematics, cobordism is a fundamental equivalence relation on the class of compact manifolds of the same dimension, set up using the concept of the boundary (French bord, giving cobordism) of a manifold.
New!!: Curry–Howard correspondence and Cobordism · See more »
Combinatory logic
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic.
New!!: Curry–Howard correspondence and Combinatory logic · See more »
Computer program
A computer program is a collection of instructions for performing a specific task that is designed to solve a specific class of problems.
New!!: Curry–Howard correspondence and Computer program · See more »
Conditional proof
A conditional proof is a proof that takes the form of asserting a conditional, and proving that the antecedent of the conditional necessarily leads to the consequent.
New!!: Curry–Howard correspondence and Conditional proof · See more »
Continuation
In computer science and computer programming, a continuation is an abstract representation of the control state of a computer program.
New!!: Curry–Howard correspondence and Continuation · See more »
Continuation-passing style
In functional programming, continuation-passing style (CPS) is a style of programming in which control is passed explicitly in the form of a continuation.
New!!: Curry–Howard correspondence and Continuation-passing style · See more »
Coq
In computer science, Coq is an interactive theorem prover.
New!!: Curry–Howard correspondence and Coq · See more »
Corecursion
In computer science, corecursion is a type of operation that is dual to recursion.
New!!: Curry–Howard correspondence and Corecursion · See more »
Correctness (computer science)
In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification.
New!!: Curry–Howard correspondence and Correctness (computer science) · See more »
Currying
In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments (or a tuple of arguments) into evaluating a sequence of functions, each with a single argument.
New!!: Curry–Howard correspondence and Currying · See more »
Dag Prawitz
Dag Prawitz (born 1936, Stockholm) is a Swedish philosopher and logician.
New!!: Curry–Howard correspondence and Dag Prawitz · See more »
Data type
In computer science and computer programming, a data type or simply type is a classification of data which tells the compiler or interpreter how the programmer intends to use the data.
New!!: Curry–Howard correspondence and Data type · See more »
Deduction theorem
In mathematical logic, the deduction theorem is a metatheorem of propositional and first-order logic.
New!!: Curry–Howard correspondence and Deduction theorem · See more »
Dependent type
In computer science and logic, a dependent type is a type whose definition depends on a value.
New!!: Curry–Howard correspondence and Dependent type · See more »
Dialectica interpretation
In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic.
New!!: Curry–Howard correspondence and Dialectica interpretation · See more »
Double-negation translation
In proof theory, a discipline within mathematical logic, double-negation translation, sometimes called negative translation, is a general approach for embedding classical logic into intuitionistic logic, typically by translating formulas to formulas which are classically equivalent but intuitionistically inequivalent.
New!!: Curry–Howard correspondence and Double-negation translation · See more »
Elsevier
Elsevier is an information and analytics company and one of the world's major providers of scientific, technical, and medical information.
New!!: Curry–Howard correspondence and Elsevier · See more »
Evaluation strategy
Evaluation strategies are used by programming languages to determine when to evaluate the argument(s) of a function call (for function, also read: operation, method, or relation) and what kind of value to pass to the function.
New!!: Curry–Howard correspondence and Evaluation strategy · See more »
Existential quantification
In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some".
New!!: Curry–Howard correspondence and Existential quantification · See more »
Formal system
A formal system is the name of a logic system usually defined in the mathematical way.
New!!: Curry–Howard correspondence and Formal system · See more »
Function type
In computer science, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or returning a function.
New!!: Curry–Howard correspondence and Function type · See more »
Functional programming
In computer science, functional programming is a programming paradigm—a style of building the structure and elements of computer programs—that treats computation as the evaluation of mathematical functions and avoids changing-state and mutable data.
New!!: Curry–Howard correspondence and Functional programming · See more »
Genetic programming
In artificial intelligence, genetic programming (GP) is a technique whereby computer programs are encoded as a set of genes that are then modified (evolved) using an evolutionary algorithm (often a genetic algorithm, "GA") – it is an application of (for example) genetic algorithms where the space of solutions consists of computer programs.
New!!: Curry–Howard correspondence and Genetic programming · See more »
Georg Kreisel
Georg Kreisel FRS (September 15, 1923 – March 1, 2015) was an Austrian-born mathematical logician who studied and worked in Great Britain and America.
New!!: Curry–Howard correspondence and Georg Kreisel · See more »
Gerhard Gentzen
Gerhard Karl Erich Gentzen (November 24, 1909 – August 4, 1945) was a German mathematician and logician.
New!!: Curry–Howard correspondence and Gerhard Gentzen · See more »
Grothendieck topology
In category theory, a branch of mathematics, a Grothendieck topology is a structure on a category C which makes the objects of C act like the open sets of a topological space.
New!!: Curry–Howard correspondence and Grothendieck topology · See more »
Haskell Curry
Haskell Brooks Curry (September 12, 1900 – September 1, 1982) was an American mathematician and logician.
New!!: Curry–Howard correspondence and Haskell Curry · See more »
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics.
New!!: Curry–Howard correspondence and Higher-order logic · See more »
Hilbert system
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob FregeMáté & Ruzsa 1997:129 and David Hilbert.
New!!: Curry–Howard correspondence and Hilbert system · See more »
Homotopy
In topology, two continuous functions from one topological space to another are called homotopic (from Greek ὁμός homós "same, similar" and τόπος tópos "place") if one can be "continuously deformed" into the other, such a deformation being called a homotopy between the two functions.
New!!: Curry–Howard correspondence and Homotopy · See more »
Homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT) refers to various lines of development of intensional type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.
New!!: Curry–Howard correspondence and Homotopy type theory · See more »
Hypothesis
A hypothesis (plural hypotheses) is a proposed explanation for a phenomenon.
New!!: Curry–Howard correspondence and Hypothesis · See more »
Initial and terminal objects
In category theory, a branch of mathematics, an initial object of a category C is an object I in C such that for every object X in C, there exists precisely one morphism I → X. The dual notion is that of a terminal object (also called terminal element): T is terminal if for every object X in C there exists a single morphism X → T. Initial objects are also called coterminal or universal, and terminal objects are also called final.
New!!: Curry–Howard correspondence and Initial and terminal objects · See more »
Institute for Advanced Study
The Institute for Advanced Study (IAS) in Princeton, New Jersey, in the United States, is an independent, postdoctoral research center for theoretical research and intellectual inquiry founded in 1930 by American educator Abraham Flexner, together with philanthropists Louis Bamberger and Caroline Bamberger Fuld.
New!!: Curry–Howard correspondence and Institute for Advanced Study · See more »
Intuitionism
In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fundamental principles claimed to exist in an objective reality.
New!!: Curry–Howard correspondence and Intuitionism · See more »
Intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof.
New!!: Curry–Howard correspondence and Intuitionistic logic · See more »
Intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
New!!: Curry–Howard correspondence and Intuitionistic type theory · See more »
Joachim Lambek
Joachim "Jim" Lambek (5 December 1922 – 23 June 2014) was Peter Redpath Emeritus Professor of Pure Mathematics at McGill University, where he earned his Ph.D. degree in 1950 with Hans Zassenhaus as advisor.
New!!: Curry–Howard correspondence and Joachim Lambek · See more »
Kurt Gödel
Kurt Friedrich Gödel (April 28, 1906 – January 14, 1978) was an Austrian, and later American, logician, mathematician, and philosopher.
New!!: Curry–Howard correspondence and Kurt Gödel · See more »
L. E. J. Brouwer
Luitzen Egbertus Jan Brouwer (27 February 1881 – 2 December 1966), usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, who worked in topology, set theory, measure theory and complex analysis.
New!!: Curry–Howard correspondence and L. E. J. Brouwer · See more »
Lambda calculus
Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.
New!!: Curry–Howard correspondence and Lambda calculus · See more »
Lambda-mu calculus
In mathematical logic and computer science, the lambda-mu calculus is an extension of the lambda calculus introduced by M. Parigot.
New!!: Curry–Howard correspondence and Lambda-mu calculus · See more »
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter.
New!!: Curry–Howard correspondence and Linear logic · See more »
Logic
Logic (from the logikḗ), originally meaning "the word" or "what is spoken", but coming to mean "thought" or "reason", is a subject concerned with the most general laws of truth, and is now generally held to consist of the systematic study of the form of valid inference.
New!!: Curry–Howard correspondence and Logic · See more »
Logic for Programming, Artificial Intelligence and Reasoning
The International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is an academic conference aiming at discussing cutting-edge results in the fields of automated reasoning, computational logic, programming languages and their applications.
New!!: Curry–Howard correspondence and Logic for Programming, Artificial Intelligence and Reasoning · See more »
Logic programming
Logic programming is a type of programming paradigm which is largely based on formal logic.
New!!: Curry–Howard correspondence and Logic programming · See more »
Logical conjunction
In logic, mathematics and linguistics, And (∧) is the truth-functional operator of logical conjunction; the and of a set of operands is true if and only if all of its operands are true.
New!!: Curry–Howard correspondence and Logical conjunction · See more »
Logical consequence
Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically follows from one or more statements.
New!!: Curry–Howard correspondence and Logical consequence · See more »
Logical disjunction
In logic and mathematics, or is the truth-functional operator of (inclusive) disjunction, also known as alternation; the or of a set of operands is true if and only if one or more of its operands is true.
New!!: Curry–Howard correspondence and Logical disjunction · See more »
Mathematical induction
Mathematical induction is a mathematical proof technique.
New!!: Curry–Howard correspondence and Mathematical induction · See more »
Mathematical proof
In mathematics, a proof is an inferential argument for a mathematical statement.
New!!: Curry–Howard correspondence and Mathematical proof · See more »
Mathematician
A mathematician is someone who uses an extensive knowledge of mathematics in his or her work, typically to solve mathematical problems.
New!!: Curry–Howard correspondence and Mathematician · See more »
Modal logic
Modal logic is a type of formal logic primarily developed in the 1960s that extends classical propositional and predicate logic to include operators expressing modality.
New!!: Curry–Howard correspondence and Modal logic · See more »
Model of computation
In computer science, and more specifically in computability theory and computational complexity theory, a model of computation is a model which describes how a set of outputs are computed given a set of inputs.
New!!: Curry–Howard correspondence and Model of computation · See more »
Modus ponens
In propositional logic, modus ponens (MP; also modus ponendo ponens (Latin for "mode that affirms by affirming") or implication elimination) is a rule of inference.
New!!: Curry–Howard correspondence and Modus ponens · See more »
Monad (functional programming)
In functional programming, a monad is a design pattern that defines how functions, actions, inputs, and outputs can be used together to build generic types, with the following organization.
New!!: Curry–Howard correspondence and Monad (functional programming) · See more »
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning.
New!!: Curry–Howard correspondence and Natural deduction · See more »
Nicolaas Govert de Bruijn
Nicolaas Govert (Dick) de Bruijn (9 July 1918 – 17 February 2012) was a Dutch mathematician, noted for his many contributions in the fields of analysis, number theory, combinatorics and logic.
New!!: Curry–Howard correspondence and Nicolaas Govert de Bruijn · See more »
Normalization property (abstract rewriting)
In mathematical logic and theoretical computer science, a rewrite system has the (strong) normalization property or is terminating if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates with an irreducible term, also called a normal form.
New!!: Curry–Howard correspondence and Normalization property (abstract rewriting) · See more »
Oxford University Press
Oxford University Press (OUP) is the largest university press in the world, and the second oldest after Cambridge University Press.
New!!: Curry–Howard correspondence and Oxford University Press · See more »
Peirce's law
In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce.
New!!: Curry–Howard correspondence and Peirce's law · See more »
Per Martin-Löf
Per Erik Rutger Martin-Löf (born May 8, 1942) is a Swedish logician, philosopher, and mathematical statistician.
New!!: Curry–Howard correspondence and Per Martin-Löf · See more »
Peter Johnstone (mathematician)
Peter Tennant Johnstone (born 1948) is Professor of the Foundations of Mathematics at the University of Cambridge, and a fellow of St. John's College.
New!!: Curry–Howard correspondence and Peter Johnstone (mathematician) · See more »
Principal type
In type theory, a type system is said to have the principal type property if, given a term and an environment, there exists a principal type for this term in this environment, i.e. a type such that all other types for this term in this environment are an instance of the principal type.
New!!: Curry–Howard correspondence and Principal type · See more »
Product type
In programming languages and type theory, a product of types is another, compounded, type in a structure.
New!!: Curry–Howard correspondence and Product type · See more »
Programming language
A programming language is a formal language that specifies a set of instructions that can be used to produce various kinds of output.
New!!: Curry–Howard correspondence and Programming language · See more »
Programming language theory
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features.
New!!: Curry–Howard correspondence and Programming language theory · See more »
Proof calculus
In mathematical logic, a proof calculus or a proof system is built to prove statements.
New!!: Curry–Howard correspondence and Proof calculus · See more »
Proof net
In proof theory, proof nets are a geometrical method of representing proofs that eliminates two forms of bureaucracy that differentiates proofs: (A) irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and (B) the order of rules applied in a derivation.
New!!: Curry–Howard correspondence and Proof net · See more »
Proof theory
Proof theory is a major branchAccording to Wang (1981), pp.
New!!: Curry–Howard correspondence and Proof theory · See more »
Proof-carrying code
Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code.
New!!: Curry–Howard correspondence and Proof-carrying code · See more »
Realizability
In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.
New!!: Curry–Howard correspondence and Realizability · See more »
Recursion (computer science)
Recursion in computer science is a method of solving a problem where the solution depends on solutions to smaller instances of the same problem (as opposed to iteration).
New!!: Curry–Howard correspondence and Recursion (computer science) · See more »
Relevance logic
Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related.
New!!: Curry–Howard correspondence and Relevance logic · See more »
Return type
In computer programming, the return type (or result type) defines and constrains the data type of the value returned from a subroutine or method.
New!!: Curry–Howard correspondence and Return type · See more »
Rule of inference
In logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions).
New!!: Curry–Howard correspondence and Rule of inference · See more »
Sequent
In mathematical logic, a sequent is a very general kind of conditional assertion.
New!!: Curry–Howard correspondence and Sequent · See more »
Sequent calculus
Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology.
New!!: Curry–Howard correspondence and Sequent calculus · See more »
Set theory
Set theory is a branch of mathematical logic that studies sets, which informally are collections of objects.
New!!: Curry–Howard correspondence and Set theory · See more »
Simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types.
New!!: Curry–Howard correspondence and Simply typed lambda calculus · See more »
Springer Science+Business Media
Springer Science+Business Media or Springer, part of Springer Nature since 2015, is a global publishing company that publishes books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing.
New!!: Curry–Howard correspondence and Springer Science+Business Media · See more »
Stephen Cole Kleene
Stephen Cole Kleene (January 5, 1909 – January 25, 1994) was an American mathematician.
New!!: Curry–Howard correspondence and Stephen Cole Kleene · See more »
String theory
In physics, string theory is a theoretical framework in which the point-like particles of particle physics are replaced by one-dimensional objects called strings.
New!!: Curry–Howard correspondence and String theory · See more »
Substructural type system
Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances.
New!!: Curry–Howard correspondence and Substructural type system · See more »
System F
System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types.
New!!: Curry–Howard correspondence and System F · See more »
Tagged union
In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, or sum type, is a data structure used to hold a value that could take on several different, but fixed, types.
New!!: Curry–Howard correspondence and Tagged union · See more »
Tautology (logic)
In logic, a tautology (from the Greek word ταυτολογία) is a formula or assertion that is true in every possible interpretation.
New!!: Curry–Howard correspondence and Tautology (logic) · See more »
Thierry Coquand
Thierry Coquand (born 18 April 1961 in Jallieu, Isère, France) is a professor in computer science at the University of Gothenburg, Sweden.
New!!: Curry–Howard correspondence and Thierry Coquand · See more »
Total functional programming
Total functional programming (also known as strong functional programming, to be contrasted with ordinary, or weak functional programming) is a programming paradigm that restricts the range of programs to those that are provably terminating.
New!!: Curry–Howard correspondence and Total functional programming · See more »
Turing completeness
In computability theory, a system of data-manipulation rules (such as a computer's instruction set, a programming language, or a cellular automaton) is said to be Turing complete or computationally universal if it can be used to simulate any Turing machine.
New!!: Curry–Howard correspondence and Turing completeness · See more »
Turing machine
A Turing machine is a mathematical model of computation that defines an abstract machine, which manipulates symbols on a strip of tape according to a table of rules.
New!!: Curry–Howard correspondence and Turing machine · See more »
Type inhabitation
In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type \tau and a typing environment \Gamma, does there exist a \lambda-term M such that \Gamma \vdash M: \tau? With an empty type environment, such an M is said to be an inhabitant of \tau.
New!!: Curry–Howard correspondence and Type inhabitation · See more »
Type rule
In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction.
New!!: Curry–Howard correspondence and Type rule · See more »
Type system
In programming languages, a type system is a set of rules that assigns a property called type to the various constructs of a computer program, such as variables, expressions, functions or modules.
New!!: Curry–Howard correspondence and Type system · See more »
Type theory
In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics.
New!!: Curry–Howard correspondence and Type theory · See more »
Typed assembly language
In computer science, a typed assembly language (TAL) is an assembly language that is extended to include a method of annotating the datatype of each value that is manipulated by the code.
New!!: Curry–Howard correspondence and Typed assembly language · See more »
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction.
New!!: Curry–Howard correspondence and Typed lambda calculus · See more »
Unifying theories in mathematics
There have been several attempts in history to reach a unified theory of mathematics.
New!!: Curry–Howard correspondence and Unifying theories in mathematics · See more »
Unit type
In the area of mathematical logic and computer science known as type theory, a unit type is a type that allows only one value (and thus can hold no information).
New!!: Curry–Howard correspondence and Unit type · See more »
Universal quantification
In predicate logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all".
New!!: Curry–Howard correspondence and Universal quantification · See more »
Well-formed formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.
New!!: Curry–Howard correspondence and Well-formed formula · See more »
William Alvin Howard
William Alvin Howard (born 1926) is a proof theorist best known for his work demonstrating formal similarity between intuitionistic logic and the simply typed lambda calculus that has come to be known as the Curry–Howard correspondence.
New!!: Curry–Howard correspondence and William Alvin Howard · See more »
Redirects here:
C-H correspondence, C-H equivalence, C-H isomorphism, C-H-L correspondence, C-H-L equivalence, C-H-L isomorphism, C.H. correspondence, C.H. equivalence, C.H. isomorphism, C.H.L. correspondence, C.H.L. equivalence, C.H.L. isomorphism, CH correspondence, CH equivalence, CH isomorphism, CHL correspondence, CHL equivalence, CHL isomorphism, Curry Howard, Curry Howard isomorphism, Curry-Howard, Curry-Howard Correspondence, Curry-Howard Isomorphism, Curry-Howard correspondence, Curry-Howard equivalence, Curry-Howard isomorphism, Curry-Howard-Lambek isomorphism, Curry–Howard, Curry–Howard equivalence, Curry–Howard isomorphism, Curry–Howard–Lambek correspondence, Curry–Howard–Lambek isomorphism, C–H correspondence, C–H equivalence, C–H isomorphism, Formulae as types, Formulae-as-types, Formulae-as-types correspondence, Programs as proofs, Programs-as-proofs, Proofs as Programs interpretation, Proofs as programs, Proofs as programs interpretation, Proofs-as-Programs interpretation, Proofs-as-programs, Proofs-as-programs interpretation, Propositions as Types, Propositions as Types interpretation, Propositions as types, Propositions as types interpretation, Propositions as types principle, Propositions-as-Types, Propositions-as-Types interpretation, Propositions-as-types, Propositions-as-types interpretation.
References
[1] https://en.wikipedia.org/wiki/Curry–Howard_correspondence
