Introduced in a book of Michel Breal, it refers to the study of how words change their meanings.

Russell’s paradox shows that every set theory that contains an unrestricted comprehension principle leads to contradictions.

Introduced by Russell, a definition is impredicative if it mentions or quantifies over the set being defined.

Written by Whitehead and Russell, and aims to express mathmatical propositions via symbolic logic to the greatest extent.

Introduced by Moses Schönfinkel and Haskell Curry, it's computational system based on abstraction elimination.

Posed by David Hilbert and Wilhelm Ackermann, it's a challenge that asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid.

Introduced by Alonzo Church, λ-calculus is a formal system in mathmatical logic for expressing computation based on function abstraction and application using variable binding and substitution.

Introduced by Alonzo Church, it's a means of representing data and operators in the lambda calculus.

Published by Kurt Gödel, they show that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

Proved by Gerhard Gentzen, it corresponds to the strong normalization property in higher-order typed lambda calculus.

Invented by Alan Turing, it's a mathmatical model of computation that defines an abstract machine that manipulates symbols on a strip of tape according to a table of rules.

Proved by Alonzo Church and J.Barkley Rosser, it states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.

Introduced by Alonzo Church, STLC is a typed interpretation of the lambda calculus with only one type constructor: function types.

Kleene presented and proved a theorem which states that all three of these methods of defining languages are equivalent: regular expression, finite automaton and transition graph.

Described by Noam Chomsky, it is a containment hierarchy of classes of formal grammars.

Invented by John Backus, it's a imperative language intended for scientific computing.

Introduced by Curry and Feys, aims to provide an analogous way to build up functions and to remove any mention of variables in predicate logic.

Developed by John McCarthy, Lisp (LISt Processing) is a symbolic computational language.

Proposed by John Backus in ALGOL 58, BNF is a metasyntax notation for context-free grammars.

Originated in ALGOL 60, it states that name resolution depends on the location in the source code and the lexical context.

Proposed by Dana Scott, it's a way to represent (recursive) data types in the lambda calculus.

Developed by Ole-Johan Dahl and Kristen Nygaard, it’s the first object-oriented programming language.

Described by Peter J. Landin, it's an abstract machine intended as a target for functional programming language compilers.

Devised by Peter Landin in “The Next 700 Programming Languages”, it’s a abstract imperative programming language with functional core.

Introduced by Christopher Strachey, it's also known as funtion overloading.

Proposed by Tony Hoare in "An axiomatic basis for computer programming", it's a formal system for reasoning about the correctness of computer programs.

Proposed by Haskell Curry and William Alvin Howard, it's a correspondence between the programs of simply typed lambda calculus and the proofs of natural deduction.

Proposed by D. S. Scott, it’s a topological model for λ-calculus.

First developed by Chris Wadsworth, it's an efficient implementation of non-strict evaluation.

Invented by De Bruijn, it's a tool to represent terms of lambda calculus without naming the bound variables.

Designed by Alain Colmerauer and Robert Kowalski, it's a logical programming language based on unification.

Proposed by Jean-Yves Girard, it's the type-theoretic analogue of Russell's paradox in set theory.

Created by Per Martin-Löf, it's a type theory on the principles of mathematical constructivism.

Designed by Alan Kay. Smalltalk is a object-oriented language based on the idea of message passing.

Independently discovered by Jean-Yves Girard and John C. Reynolds, it’s a typed lambda calculus by introducing universal quantification over types.

Designed by Dennis Ritchie, it's a precedure-based language for Unix programming.

Originated in MIT AI Lab, Lisp Machine is a high-level language computer architecture that supports effective garbage collection, windowing systems etc.

Designed by Robin Milner, it’s a type-safe functional programming language.

First proposed by Barbara Liskov and Stephen N. Zilles, it's a mathmatical model for data types.

Developed at IBM by Donald D. Chamberlin and Raymond F. Boyce, it's a DSL for managing data in relational database.

Developed by Guy L. Steele and Gerald Jay Sussman, it's a S-expression language based on λ-calculus.

First observed by John Reynolds, later formulated by Philip Wadler, it's a challenge problem that concerns the extensibility and modularity of statically typed data abstractions.

First introduced in ML, it's one kind of polymorphism where function and datetype can be written generically so that it can handle values identically without depending on their types.

Presented by John Backus in "Can Programming Be Liberated From the von Neumann Style? A Functional Style and its Algebra of Programs".

Independently presented by J. Roger Hindley and Robin Milner, it's a classical type system for λ-calculus with parametric polymorphism.

Originated in Hope, it's commonly considered as product type and sum type.

Formalized by John C. Reynolds, it's a form of polymorphism where types can be subsumed by its subtypes.

Developed by Brad Cox and Tom Love, it's an extension of C language with Smalltalk-style object system.

Created by Bjarne Stroustrup, it's an extension of C language with object system, templates and the STL.

Designed by R. Kent Dybvig, it's an implementation of Scheme and uses an incremental native-code compiler to produce native binary files.

Designed by Richard Stallman, it's a scripting Lisp dialect for Emacs.

Originated in Flavors, mixins is an inheritance model that can subsumes multiple-inheritance etc.

Created by Coquand and Huet, it's a higher-order typed lambda calculus with strong normalization.

Proposed by Luca Cardelli, it's a property "If A is a compile-time term and B is a subterm of A, then B must also be a compile-time term."

Based on calculus of inductive constructions, it's an interactive theorem prover.

Introduced by Mitchell Wand, it's a kind of polymorphism that allows one to write programs that are polymorphic on record field types.

Presented by Wadler and Blott in "How to make ad-hoc polymorphism less ad hoc", it’s a type system construct that solves overloading.

CLOS is a dynamic object system that supports multiple dispatch and multiple inheritance.

Named after Haskell Curry, it's a pure typed functional programming language.

Introduced by Henk Barendregt, it's a framework that tries to generalize CoC from λ-calculus in three dimensions.

Developed by Guido van Rossum, it's a dynamic language that emphasizes code readability.

GHC is a modern Haskell Compiler lead by Simon Peyton Jones et al..

Designed by Roberto Ierusalimschy, it's a lightweight language intended for embedded use in applications.

Introduced by Sun Microsystems, it's a virtual machine thats run Java bytecode.

Designed by James Gosling, it's a typed OOP language that runs on JVM.

Designed by Yukihiro Matsumoto, it’s a pure OOP scripting language with metaprogramming.

Founded by Matthias Felleisen as a research group, it's designed as a platform for programming language design and implementation.

Stated by Yoshiki Kinoshita, it's an abstract result on functors of the type morphisms into a fixed object.

Created in 1996 by Xavier Leroy et al., it's a dialect of ML with an object system.

Designed at Microsoft by Anders Hejlsberg, it's a typed OOP language that runs on .NET.

Proposed by Atsushi Igarashi et al, it’s a minimal java-like language which models inheritance and subtyping.

Proposed by Oscar Nierstrasz et al., traits is a simple compositional model for structuring object-oriented programs.

Designed by Martin Odersky, it's a strongly typed language on the idea of combining object-oriented and functional programming.

Proposed by J. Nathan Foster et al., it's a solution to view-update problem via bi-directional tree transformations.

Developed by Xavier Leroy, it's a formally verified optimizing compiler for a large subset of CLight.

Developed by Jeremy Siek and Walid Taha, it's a type system that allows parts of a program to be dynamically typed and other parts to be statically typed.

Designed by Rich Hickey, it's a functional dialect of Lisp running on JVM.

Designed by Google, it's a static language for concurrent programming.

Designed at Mozilla by Graydon Hoare, it's a static language that emphasizes memory safety.