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

1901Russell's Paradox

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.

1910Principia Mathematica

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

1924SKI Combinator Calculus

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.

1930Lambda Calculus (λ-calculus)

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.

1930Church Encoding

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

1931Gödel's Incompleteness Theorems

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.

1934Cut-Elimination Theorem

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

1936Turing Machine

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.

1936Church-Rosser Theorem

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.

1940Simply Typed Lambda Calculus (STLC)

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

1954Kleene's Theorem

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.

1956Chomsky Hierarchy

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.

1958Combinatory Logic

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.

1959Backus-Naur Form (BNF)

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

1960Lexical Scoping

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

1962Scott Encoding

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.

1964SECD Machine (Stack, Environment, Control, Dump)

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

1966ISWIM (If you See What I Mean)

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

1967Ad-hoc Polymorphism

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

1969Hoare Logic

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

1969Curry-Howard Isomorphism

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.

1969Scott Topology

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

1971Graph Reducation

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

1972De Bruijn Index

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.

1972Girard's Paradox

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

1972Intuitionistic Type 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.

1972System F

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.

1973Lisp Machine

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.

1974Abstract Data Type (ADT)

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.

1975Expression Problem

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.

1975Parametric Polymorphism

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.

1977Functional Programming (FP)

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

1978Hindley–Milner Type System (HM)

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

1980Algebraic Data Type

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

1980Subtyping Polymorphism

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.

1985Chez Scheme

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

1985Emacs Lisp

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.

1988Calculus of Constructions (CoC)

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

1988Phase Distinction

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."

1989Coq Proof Assistant

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

1989Row Polymorphism

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

1989Type Class

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

1990Common Lisp Object System (CLOS)

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.

1991Lambda Cube (λ-cube)

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.

1992Glasgow Haskell Compiler (GHC)

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.

1994Java Virtual Machine (JVM)

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.

1995Racket (PLT Scheme)

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

1996Yoneda Lemma

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.

2001Featherweight Java

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.

2006Gradual Typing

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.