Foundational concepts

• Programming paradigm
  Programming paradigm
  A programming paradigm is a fundamental style of computer programming. Paradigms differ in the concepts and abstractions used to represent the elements of a program and the steps that compose a computation A programming paradigm is a fundamental style of computer programming. (Compare with a...
  
  
• Declarative programming
  Declarative programming
  In computer science, declarative programming is a programming paradigm that expresses the logic of a computation without describing its control flow. Many languages applying this style attempt to minimize or eliminate side effects by describing what the program should accomplish, rather than...
  
  
• Programs as mathematical objects
• Function-level programming
  Function-level programming
  In computer science, function-level programming refers to one of the two contrasting programming paradigms identified by John Backus in his work on programs as mathematical objects, the other being value-level programming....
  
  
• Purely functional
  Purely functional
  Purely functional is a term in computing used to describe algorithms, data structures or programming languages that exclude destructive modifications...
  
  
• Lambda programming
• Static scoping
  Scope (programming)
  In computer programming, scope is an enclosing context where values and expressions are associated. Various programming languages have various types of scopes. The type of scope determines what kind of entities it can contain and how it affects them—or semantics...
  
  
• Higher-order function
  Higher-order function
  In mathematics and computer science, higher-order functions, functional forms, or functionals are functions which do at least one of the following:*take one or more functions as an input*output a function...
  
  
• Referential transparency

Lambda calculus

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. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...

• Currying
  Currying
  In mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...
  
  
• Lambda abstraction
• Church-Rosser theorem
• Extensionality
  Extensionality
  In logic, extensionality, or extensional equality refers to principles that judge objects to be equal if they have the same external properties...
  
  
• Church numeral

Combinatory logic

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 for the design of functional programming...

• Fixed point combinator
  Fixed point combinator
  In computer science, a fixed-point combinator is a higher-order function that computes a fixed point of other functions. A fixed point of a function f is a value x such that x = f. For example, 0 and 1 are fixed points of the function f = x2, because 0 = 02 and 1 = 12...
  
  
• SKI combinator calculus
  SKI combinator calculus
  SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped lambda calculus. It can be thought of as a computer programming language, though it is not useful for writing software...
  
  
• B,C,K,W system
  B,C,K,W system
  The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry .The combinators are defined as follows:* B x...
  
  
• SECD machine
  SECD machine
  The SECD machine is a highly influential virtual machine and abstract machine intended as a target for functional programming language compilers. The letters stand for Stack, Environment, Code, Dump, the internal registers of the machine...
  
  
• Graph reduction machine
  Graph reduction machine
  A graph reduction machine is a special-purpose computer built to perform combinator calculations by graph reduction.Examples include the SKIM computer, built at the University of Cambridge Computer Laboratory, and the multiprocessor GRIP computer, built at University College London.- References...
  
  

Intuitionistic logic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

• Sequent
  Sequent
  In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...
  
  , sequent calculus
  Sequent calculus
  In proof theory and mathematical logic, sequent calculus is a 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 in 1934 as a tool for studying natural deduction in...
  
  
• Natural deduction
  Natural deduction
  In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
  
  
• Intuitionistic type theory
  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 Martin-Löf, a Swedish mathematician and philosopher,...
  
  
• BHK interpretation
  BHK interpretation
  In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov...
  
  
• Curry–Howard
• Linear logic
  Linear logic
  Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
  
  
• Game semantics
  Game semantics
  Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
  
  

Type theory

Type theory

In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...

• Typed lambda calculus
  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 depends on the calculus considered...
  
  
• Typed and untyped languages
• Type signature
  Type signature
  In computer science, a type signature or type annotation defines the inputs and outputs for a function, subroutine or method. A type signature includes at least the function name and the number of its arguments...
  
  
• Type inference
  Type inference
  Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
  
  
• Datatype
• Algebraic data type
  Algebraic data type
  In computer programming, particularly functional programming and type theory, an algebraic data type is a datatype each of whose values is data from other datatypes wrapped in one of the constructors of the datatype. Any wrapped datum is an argument to the constructor...
  
  
• Type variable
  Type variable
  In type theory and programming languages, a type variable is a mathematical variable ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond to some memory locations.Programming languages that...
  
  
• First-class value
• Polymorphism
• Calculus of constructions
  Calculus of constructions
  The calculus of constructions 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 inductive constructions.-General traits:The CoC is a...
  
  

Denotational semantics

Denotational semantics

In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...

• Domain theory
  Domain theory
  Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
  
  
  • Directed complete partial order
  • Knaster–Tarski theorem

Operational issues

• Graph reduction
  Graph reduction
  In computer science, graph reduction implements an efficient version of non-strict evaluation, an evaluation strategy where the arguments to a function are not immediately evaluated. This form of non-strict evaluation is also known as lazy evaluation and used in functional programming languages...
  
  
  • Combinator graph reduction
• Non-strict programming language
• Lazy evaluation
  Lazy evaluation
  In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
  
  , eager evaluation
  Eager evaluation
  In computer programming, eager evaluation or greedy evaluation is the evaluation strategy in most traditional programming languages. In eager evaluation an expression is evaluated as soon as it gets bound to a variable. The term is typically used to contrast lazy evaluation, where expressions are...
  
  
• Speculative evaluation
• Side-effect
• Assignment
  Assignment (computer science)
  In computer programming, an assignment statement sets or re-sets the value stored in the storage location denoted by a variable name. In most imperative computer programming languages, assignment statements are one of the basic statements...
  
  
  • Setq
• Closure
  Closure (computer science)
  In computer science, a closure is a function together with a referencing environment for the non-local variables of that function. A closure allows a function to access variables outside its typical scope. Such a function is said to be "closed over" its free variables...
  
  
• Continuation
  Continuation
  In computer science and programming, a continuation is an abstract representation of the control state of a computer program. A continuation reifies the program control state, i.e...
  
  
• Continuation passing style
• Operational semantics
  Operational semantics
  In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
  
  
• State transition system
  State transition system
  In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
  
  
• Simulation preorder
  Simulation preorder
  In theoretical computer science a simulation preorder is a relation between state transition systems associating systems which behave in the same way in the sense that one system simulates the other....
  
  
• Bisimulation
  Bisimulation
  In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
  
  
• Monads in functional programming
  Monads in functional programming
  In functional programming, a monad is a programming structure that represents computations. Monads are a kind of abstract data type constructor that encapsulate program logic instead of data in the domain model...
  
  
• Exception handling
  Exception handling
  Exception handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....
  
  
• Garbage collection (computer science)
  Garbage collection (computer science)
  In computer science, garbage collection is a form of automatic memory management. The garbage collector, or just collector, attempts to reclaim garbage, or memory occupied by objects that are no longer in use by the program...
  
  

Languages

• Abstract Rewriting Machine
  Abstract Rewriting Machine
  The Abstract Rewriting Machine is a virtual machine which implements term rewriting for minimal term rewriting systems.Minimal term rewriting systems are left-linear term rewriting systems in which each rule takes on one of six forms:...
  
  
• Clean programming language
  Clean programming language
  In computer science, Clean is a general-purpose purely functional computer programming language.-Features:The language Clean first appeared in 1987 and is still further developed; it shares many properties with Haskell:...
  
  
• Clojure programming language
  Clojure
  Clojure |closure]]") is a recent dialect of the Lisp programming language created by Rich Hickey. It is a general-purpose language supporting interactive development that encourages a functional programming style, and simplifies multithreaded programming....
  
  
• Erlang programming language
  Erlang programming language
  Erlang is a general-purpose concurrent, garbage-collected programming language and runtime system. The sequential subset of Erlang is a functional language, with strict evaluation, single assignment, and dynamic typing. For concurrency it follows the Actor model. It was designed by Ericsson to...
  
  
• FP programming language
  FP programming language
  FP is a programming language created by John Backus to support the function-level programming paradigm...
  
  
• F# programming language
  F Sharp programming language
  F# is a multi-paradigm programming language, targeting the .NET Framework, that encompasses functional programming as well as imperative and object-oriented programming disciplines. It is a variant of ML and is largely compatible with the OCaml implementation...
  
  
• Haskell programming language
  Haskell (programming language)
  Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
  
  
  • Glasgow Haskell Compiler
    Glasgow Haskell Compiler
    The Glorious Glasgow Haskell Compilation System, more commonly known as the Glasgow Haskell Compiler or GHC, is an open source native code compiler for the functional programming language Haskell. The lead developers are Simon Peyton Jones and Simon Marlow...
    
    
  • Gofer
    Gofer (software)
    Gofer is an implementation of the programming language Haskell intended for educational purposes and supporting a language based on version 1.2 of the Haskell report. It has since been replaced by Hugs....
    
    
  • Hugs
    Hugs
    Hugs , also Hugs 98, is a bytecode interpreter for the functional programming language Haskell. Hugs is the successor to Gofer, and was originally derived from Gofer version 2.30b. Hugs and Gofer were originally developed by Mark P. Jones, now a professor at Portland State University.Hugs comes...
    
    
  • Template Haskell
    Template Haskell
    Template Haskell is an experimental language extension to the programming language Haskell implemented in the Glasgow Haskell Compiler . In early incarnations it was also known as Template Meta-Haskell....
    
    
• ISWIM
  ISWIM
  ISWIM is an abstract computer programming language 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...
  
  
• Kent Recursive Calculator
  Kent Recursive Calculator
  KRC is a lazy functional language developed by David Turner in 1981 based on SASL, with pattern matching, guards and ZF expressions ....
  
  
• Kogut programming language
• Lisp
  Lisp programming language
  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 Fortran is older...
  
  
  • AutoLISP
    AutoLISP
    AutoLISP is a dialect of Lisp programming language built specifically for use with the full version of AutoCAD and its derivatives, which include AutoCAD Map 3D, AutoCAD Architecture and AutoCAD Mechanical...
    
    
  • Common Lisp
    Common Lisp
    Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
    
    
  • Emacs Lisp
    Emacs Lisp
    Emacs Lisp is a dialect of the Lisp programming language used by the GNU Emacs and XEmacs text editors . It is used for implementing most of the editing functionality built into Emacs, the remainder being written in C...
    
    
  • Scheme programming language
  • Lush programming language
• Mercury programming language
  Mercury programming language
  Mercury is a functional logic programming language geared towards real-world applications. It is developed at the University Of Melbourne Computer Science department under the supervision of Zoltan Somogyi. The first version was developed by Fergus Henderson, Thomas Conway and Zoltan Somogyi and...
  
  
• Miranda programming language
  Miranda programming language
  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...
  
  
• ML programming language
  ML programming language
  ML is a general-purpose functional programming language developed by Robin Milner and others in the early 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM...
  
   (:Category:ML programming language family)
  • Mythryl
  • Objective Caml
    Objective Caml
    OCaml , originally known as Objective Caml, 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...
    
    
  • Standard ML
    Standard ML
    Standard ML 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 provers.SML is a modern descendant of the ML...
    
    
• Pure
  Pure (programming language)
  Pure is a dynamically typed, functional programming language based on term rewriting. It has facilities for user-defined operator syntax, macros, multiple-precision numbers, and compilation to native code through the LLVM...
  
  
• Q (equational programming language)
• Q (programming language from Kx Systems)
  Q (programming language from Kx Systems)
  Q is a proprietary array processing language developed by Arthur Whitney and commercialized by Kx Systems. The language serves as the query language for kdb+, a disk based and in-memory, column-based database. kdb+ is based upon K, a terse variant of APL...
  
  
• Quantum programming
  Quantum programming
  Quantum programming is a set of computer programming languages that allow the expression of quantum algorithms using high-level constructs. The point of quantum languages is not so much to provide a tool for programmers, but to provide tools for researchers to understand better how quantum...
  
  
• Scala
• SISAL
  SISAL
  SISAL is a general-purpose single assignment functional programming language with strict semantics, implicit parallelism, and efficient array handling. SISAL outputs a dataflow graph in Intermediary Form 1...
  
  
• Ωmega