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.
55 Topic topics matching:
Filter this Collection| x name | x image | x article |
|---|---|---|
| x Gottlob Frege |
|
Friedrich Ludwig Gottlob Frege (8 November 1848 – 26 July 1925) was a German mathematician who became a logician and philosopher. He was one of the founders of modern logic, and made major contributions to the foundations of mathematics. As a...
|
| x Bertrand Russell |
|
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS (18 May 1872 – 2 February 1970) was an English philosopher, logician, mathematician, historian, socialist, pacifist and social critic. Although he spent the majority of his life in England,...
|
| x Gerhard Gentzen |
|
Gerhard Karl Erich Gentzen (November 24, 1909, Greifswald, Germany – August 4, 1945, Prague, Czechoslovakia) was a German mathematician and logician.
Gentzen was a student of Paul Bernays at the University of Göttingen. Bernays was fired as "non...
|
| x Alonzo Church |
|
Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church...
|
| x Haskell Curry |
|
Haskell Brooks Curry (September 12, 1900 – September 1, 1982) was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses...
|
| x J. Roger Hindley | ||
| x Robin Milner |
|
Arthur John Robin Gorell Milner FRS FRSE (Robin Milner or A.J.R.G. Milner, born 13 January 1934 near Plymouth) is a prominent British computer scientist.
Milner was born in Yealmpton, near Plymouth, England into a military family. He was awarded a...
|
| x Pythagoras |
|
Pythagoras of Samos (Greek: Ὁ Πυθαγόρας ὁ Σάμιος, O Pūthagoras o Samios, "Pythagoras the Samian", or simply Ὁ Πυθαγόρας; c. 570-c. 495 BC) was an Ionian Greek philosopher and founder of the religious movement called Pythagoreanism. He is often...
|
| x Jean-Yves Girard |
|
Jean-Yves Girard (born 1947 in Lyon) is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of...
|
| x Begriffsschrift |
|
Begriffsschrift is the title of a book on logic by Gottlob Frege, published in 1879, and is also the name of the formal system set out in that book.
Begriffsschrift is usually translated as concept writing or concept notation; the full title of the...
|
| x 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 ...
|
|
| x 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,...
|
| x 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...
|
|
| x 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...
|
| x William Alvin Howard |
William Alvin Howard (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. He has also...
|
|
| x Per Martin-Löf |
|
Per Erik Rutger Martin-Löf (born 1942) is a Swedish logician, philosopher, and mathematician. He is best known for developing intuitionistic type theory as a constructive foundation of mathematics. Per Martin-Löf holds a joint chair for Mathematics...
|
| x Nicolaas Govert de Bruijn |
|
Nicolaas Govert (Dick) de Bruijn (born 9 July 1918) is a Dutch mathematician, affiliated as professor emeritus with the Eindhoven University of Technology. He received his Ph.D. in 1943 from Vrije Universiteit Amsterdam.
De Bruijn covered many areas...
|
| x 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...
|
|
| x 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...
|
|
| x 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...
|
|
| x John C. Reynolds |
|
John C. Reynolds (born June 1, 1935) is an American computer scientist.
John Reynolds studied at Purdue University and then earned a PhD in theoretical physics from Harvard University in 1961. He was Professor of Information science at Syracuse...
|
| x 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...
|
|
| x Subformula property | ||
| x 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...
|
| x 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,...
|
|
| x Dag Prawitz |
|
Dag Prawitz (born 1936) is a Swedish philosopher and logician. He is best known for his work on proof theory and the foundations of natural deduction.
|
| x Robert Feys |
|
Robert Feys (1889—1961) was a Belgian logician and philosopher, who worked at the University of Leuven (Belgium).
In 1958 Feys and Haskell B. Curry devised the type inference algorithm for the simply typed lambda calculus (Combinatory Logic I).
|
| x 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...
|
|
| x ML |
ML is a general-purpose functional programming language developed by Robin Milner and others in the late 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM. Historically, ML stands for metalanguage: it was conceived to develop...
|
|
| x Standard ML |
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem...
|
|
| x Objective Caml |
|
Objective Caml, or OCaml (pronounced /oʊˈkæməl/ oh-KAM-əl) is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996. OCaml is an open source project managed...
|
| x Haskell |
|
Haskell (pronounced [ˈhæskəl]) is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry.
Following the release of Miranda by Research...
|
| x NuPRL |
NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL.
|
|
| x Kleisli |
Kleisli is a database language for biomedical data (implemented in Standard ML).
|
|
| x XDuce |
XDuce ("tranceduce") is an XML transformation language.
|
|
| x Pi-calculus |
In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems). The aim of the π...
|
|
| x Join-calculus |
The join-calculus is a process calculus developed at INRIA. The join-calculus was developed to provide a formal basis for the design of distributed programming languages, and therefore intentionally avoids communications constructs found in other...
|
|
| x HOL theorem prover |
HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language....
|
|
| x LCF theorem prover |
LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general-purpose programming language ML to allow users to write...
|
|
| x Isabelle theorem prover |
The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing...
|
|
| x Coq |
|
In computer science, Coq is a proof assistant application. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof...
|
| x Miranda |
|
Miranda is a non-strict purely functional programming language designed by David Turner as a successor to his earlier programming languages SASL and KRC, using some concepts from ML and Hope. It was produced by Research Software Ltd. of England ...
|
| x Twelf |
Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.
At its simplest, a Twelf program (called a "signature") is a collection of declarations of type...
|
|
| x Functional programming |
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative...
|
|
| x 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. The host system can quickly verify the validity of the proof...
|
|
| x 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. These annotations can then be used by a program (type checker...
|
|
| x Calculus of constructions |
The calculus of constructions (CoC) is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of...
|
|
| x ISWIM |
ISWIM is an abstract computer programming language (or a family of programming languages) devised by Peter J. Landin and first described in his article, The Next 700 Programming Languages, published in the Communications of the ACM in 1966. The...
|
|
| x Lisp |
|
Lisp (or LISP) is a family of computer programming languages with a long history and a distinctive, fully parenthesized syntax. Originally specified in 1958, Lisp is the second-oldest high-level programming language in widespread use today; only...
|
| x Lambda cube |
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the...
|
|
| x 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...
|
|
| x Timothy G. Griffin |
|
|
| x Charles Peirce |
|
Charles Sanders Peirce (pronounced /ˈpɜrs/ purse) (September 10, 1839 – April 19, 1914) was an American philosopher, logician, mathematician, and scientist, born in Cambridge, Massachusetts. Peirce was educated as a chemist and employed as a...
|
| x Philip Wadler |
|
Philip Wadler is a computer scientist well-known for his contributions to programming language design and type theory. In particular, he has contributed to the theory behind functional programming and the use of monads in functional programming, the...
|
| x Java |
|
Java refers to a number of computer software products and specifications from Sun Microsystems that together provide a system for developing application software and deploying it in a cross-platform environment. Java is used in a wide variety of...
|
