Share This
table started by
warren for the Proofs are Programs Base
There is no user-contributed description yet.
Add More Topics
Save this view to a base, or just for yourself.
18 Key Contribution topics matching:
Filter this Collection
Sort by
Date Added
↓
|
|
|
||||||
|---|---|---|---|---|---|---|---|
| x Key concept | x Date | x Contributors | x Why this is interesting | x Key artifacts | |||
| x name | x image | x article | |||||
| Russell's paradox |
|
In the foundations of mathematics, Russell's paradox (also known as Russell's antinomy), discovered by Bertrand Russell in 1901, showed that the naive set theory of Frege leads to a contradiction.
It might be assumed that, for any formal criterion,...
|
1901 | Bertrand Russell | Showed that the naive set theory of Frege leads to a contradiction -- that the set of all sets cannot contain itself. This lead the way to type theory, which allows the contradiction to be avoided. | ||
| Type inference |
Type inference, or implicit typing, refers to the ability to deduce automatically the type of a value in a programming language. It is a feature present in some strongly statically typed languages. It is often characteristic of — but not limited to ...
|
1978 | J. Roger Hindley | This is the Curry-Howard correspondence in action -- used to deduce the types of polymorphic programs from their structure and primitive operations. First discovered by the logician Hindley in 1969 and re-discovered by the computer scientist Milner in 1978. | ML | ||
| Robin Milner | |||||||
| Symbolic logic |
Symbolic logic is the area of mathematics which studies the purely formal properties of strings of symbols. The interest in this area springs from two sources. First, the symbols used in symbolic logic can be seen as representing the words used in...
|
1879 | Gottlob Frege | Revolutionized the world of logic with his book Begriffsschrift which introduced the concept of symbolic logic, thus ending the era of Aristotelian logic of the preceeding 2000 years. | Begriffsschrift | ||
| Curry–Howard correspondence |
|
The Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the...
|
1969 | Haskell Curry | Howard put together the work of Curry and Feys in 1969: proofs are programs, types are propositions, realizing the syntactic analogy between systems of formal logic and computational calculi. | The formulae-as-types notion of construction | |
| William Alvin Howard | Formulae-as-types (1969 mimeograph) | ||||||
| Intuitionistic type theory |
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per...
|
1971 | Per Martin-Löf | Martin-Lof extended the Curry-Howard correspondence to predicate logic by introducing dependent types, that is types which contain values. His Intuitionistic type theory internalizes the interpretation of intuitionistic logic proposed by Brouwer, Heyting and Kolmogorov. | |||
| Lambda calculus |
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. It was introduced by Alonzo Church in the 1930s as part of an investigation into...
|
1932 | Alonzo Church | Church developed the theory of lambda calculus as a new formulation of logical deduction, and in 1936 realized that lambda terms could be used to express every function that could ever be computed by a machine. (Turning was his student at Princeton from 1936-1938.) Church reduced all calculation to the notion of substitution. | |||
| Typed lambda calculus |
A typed lambda calculus is a typed formalism that uses the lambda-symbol (λ) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type...
|
1940 | Alonzo Church | Church introduced the typed lambda calculus to circumvent the problem of Russel's paradox as it applied to Frege's logic. This became the basis for typed programming languages like Algol and functional languages such as Haskell. | |||
| Type polymorphism |
In computer science, polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions. A function that...
|
1972 | Jean-Yves Girard | Girard showed that the second-order propositional logic can be projected into the second-order polymorphic lambda calculus with quantifiers over type variables. | System F | ||
| Type polymorphism |
In computer science, polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions. A function that...
|
1974 | John C. Reynolds | Reynolds showed that the second-order polymorphic lambda calculus can be projected into the second-order propositional logic with no loss of information. | |||
| Type polymorphism |
In computer science, polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions. A function that...
|
1975 | Robin Milner | A type theory of polymorphism in programming | |||
| Subformula property | 1934 | Gerhard Gentzen | Gentzen's subformula property eliminated diversions in the proof process and demonstrated the property of logical consistency. This paved the way for proofs to be interpreted as programs. | ||||
| Sequent calculus |
|
In proof theory and mathematical logic, sequent calculus is a widely known family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen...
|
1934 | Gerhard Gentzen | Gentzen could only demonstrate the subformula property and proof simplification for the sequent calculus, not for natural deduction. | ||
| Natural deduction logic |
A natural deduction is an instruction on how to use binary logic to move from one line to another, during a linear sequential proof. Every natural deduction, is one of the tautologies of propositional logic. As an example of a natural deduction,...
|
1934 | Gerhard Gentzen | Gentzen simplified Frege's system of deduction to reflect various axioms within the structure of the inference rules as introduction and elimination pairs. | |||
| Natural deduction logic |
A natural deduction is an instruction on how to use binary logic to move from one line to another, during a linear sequential proof. Every natural deduction, is one of the tautologies of propositional logic. As an example of a natural deduction,...
|
1956 | Dag Prawitz | Prawitz showed how to simplify Gentzen's natural deduction proofs directly. | |||
| Combinatory logic |
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis...
|
1956 | Haskell Curry | Curry and Feys defined combinators, a simplified variant of lambda expressions. Curry noted a correspondence between the types of the combinators and the laws of logic as formulated by Hilbert. | |||
| Robert Feys | |||||||
| Peirce's law |
Peirce's law in logic is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic.
In propositional calculus, Peirce's law says that ((P→Q)→P)→P. Written out, this...
|
1990 | Timothy G. Griffin | In 1990, Griffin showed that Peirce's Law is the type of the continuation operator call/cc in Scheme. This remarkable observation demonstrates the relevance of the Curry-Howard correspondence even to control operators in programming languages. | A formulae-as-types notion of control | ||
| Peirce's law |
Peirce's law in logic is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic.
In propositional calculus, Peirce's law says that ((P→Q)→P)→P. Written out, this...
|
1885 | Charles Peirce | Peirce axiomized propositional logic in the 19th century, and one of his axioms, now known as Peirce's law, implies the law of excluded middle. It wasn't until 115 years later that its relationship to programming languages was discovered. | |||
| Curry–Howard correspondence |
|
The Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. Also known as Curry–Howard isomorphism, proofs-as-programs correspondence and formulae-as-types correspondence, it refers to the...
|
2003 | Philip Wadler | Wadler shows the relationship between various programming language calling conventions to Gentzen's original sequent calculus. | Call-by-value is dual to call-by-name | |
