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.
13 Key Concept topics matching:
Filter this Collection|
|
|
||||
|---|---|---|---|---|---|
| x name | x image | x Key contribution | |||
| x Date | x Contributors | x Why this is interesting | x Key artifacts | ||
| x Type inference | 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 | |||||
| x Russell's paradox |
|
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. | |
| x Symbolic logic | 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 | |
| x Curry–Howard correspondence |
|
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 |
| 2003 | William Alvin Howard | Wadler shows the relationship between various programming language calling conventions to Gentzen's original sequent calculus. | Formulae-as-types (1969 mimeograph) | ||
| Philip Wadler | Call-by-value is dual to call-by-name | ||||
| x Intuitionistic type theory | 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. | ||
| x Lambda calculus | 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. | ||
| x Typed lambda calculus | 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. | ||
| x Type polymorphism | 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 | |
| 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. | |||
| 1975 | Robin Milner | A type theory of polymorphism in programming | |||
| x 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. | ||
| x Sequent calculus |
|
1934 | Gerhard Gentzen | Gentzen could only demonstrate the subformula property and proof simplification for the sequent calculus, not for natural deduction. | |
| x Natural deduction logic | 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. | ||
| 1956 | Dag Prawitz | Prawitz showed how to simplify Gentzen's natural deduction proofs directly. | |||
| x Combinatory logic | 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 | |||||
| x Peirce's law | 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 | |
| 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. | |||
