The Abstract Rewriting Machine (ARM) is a virtual machine which implements term rewriting for minimal term rewriting systems.
In computer programming, especially functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.
In computer programming, an assignment statement sets and/or re-sets the value stored in the storage location(s) denoted by a variable name; in other words, it copies a value into the variable.
AutoLISP is a dialect of the 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.
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 (1930).
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in the sense that one system simulates the other and vice versa.
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov.
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand.
In category theory, a category is considered Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors.
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus.
In mathematics and theoretical computer science, the Church–Rosser theorem states that, when applying reduction rules to terms in the lambda calculus, the ordering in which the reductions are chosen does not make a difference to the eventual result.
Clean is a general-purpose purely functional computer programming language.
Clojure (like "closure") is a dialect of the Lisp programming language.
In programming languages, a closure (also lexical closure or function closure) is a technique for implementing lexically scoped name binding in a language with first-class functions.
Common Lisp (CL) is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 (R2004) (formerly X3.226-1994 (R1999)).
In mathematics, the phrase complete partial order is variously used to refer to at least three similar, but distinct, classes of partially ordered sets, characterized by particular completeness properties.
In computer science and computer programming, a continuation is an abstract representation of the control state of a computer program.
In functional programming, continuation-passing style (CPS) is a style of programming in which control is passed explicitly in the form of a continuation.
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.
In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments (or a tuple of arguments) into evaluating a sequence of functions, each with a single argument.
In computer science and computer programming, a data type or simply type is a classification of data which tells the compiler or interpreter how the programmer intends to use the data.
In computer science, declarative programming is a programming paradigm—a style of building the structure and elements of computer programs—that expresses the logic of a computation without describing its control flow.
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets (posets) commonly called domains.
In computer programming, eager evaluation, also known as strict evaluation or greedy evaluation, is the evaluation strategy used by most traditional programming languages.
Elixir is a functional, concurrent, general-purpose programming language that runs on the Erlang virtual machine (BEAM).
Emacs Lisp is a dialect of the Lisp programming language used as a scripting language by Emacs (a text editor family most commonly associated with GNU Emacs and XEmacs).
Erlang is a general-purpose, concurrent, functional programming language, as well as a garbage-collected runtime system.
Exception handling is the process of responding to the occurrence, during computation, of exceptions – anomalous or exceptional conditions requiring special processing – often changing the normal flow of program execution.
In logic, extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties.
F# (pronounced F sharp) is a strongly typed, multi-paradigm programming language that encompasses functional, imperative, and object-oriented programming methods.
In programming language design, a first-class citizen (also type, object, entity, or value) in a given programming language is an entity which supports all the operations generally available to other entities.
In computer science's combinatory logic, a fixed-point combinator (or fixpoint combinator) is a higher-order function fix that, for any function f that has an attractive fixed point, returns a fixed point x of that function.
FP (short for Function Programming) is a programming language created by John Backus to support the function-level programming Backus' 1977 Turing Award lecture paradigm.
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.
In computer science, functional programming is a programming paradigm—a style of building the structure and elements of computer programs—that treats computation as the evaluation of mathematical functions and avoids changing-state and mutable data.
Game semantics (dialogische Logik, translated as dialogical logic) 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 computer science, garbage collection (GC) is a form of automatic memory management.
In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of parametric algebraic data types.
Glasgow Haskell Compiler, less commonly known as The Glorious Glasgow Haskell Compilation System or simply GHC, is an open source native code compiler for the functional programming language Haskell.
Gofer ("Good For Equational Reasoning") 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.
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.
A graph reduction machine is a special-purpose computer built to perform combinator calculations by graph reduction.
Haskell is a standardized, general-purpose compiled purely functional programming language, with non-strict semantics and strong static typing.
In mathematics and computer science, a higher-order function (also functional, functional form or functor) is a function that does at least one of the following.
Hugs (Haskell User's Gofer System), also Hugs 98, is a bytecode interpreter for the functional programming language Haskell.
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
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 Omega interpreter is a strict pure functional programming interpreter similar to the Hugs Haskell interpreter.
KRC (Kent Recursive Calculator) is a lazy functional language developed by David Turner from November 1979 to October 1981 based on SASL, with pattern matching, guards and ZF expressions (now more usually called list comprehensions).
In the mathematical areas of order and lattice theory, the Knaster–Tarski theorem, named after Bronisław Knaster and Alfred Tarski, states the following: It was Tarski who stated the result in its most general form, and so the theorem is often known as Tarski's fixed point theorem.
Kohut, Kogut, or Kohout is a surname of Slavic-language origin, meaning rooster.
Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.
In programming language theory, lazy evaluation, or call-by-need is an evaluation strategy which delays the evaluation of an expression until its value is needed (non-strict evaluation) and which also avoids repeated evaluations (sharing).
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.
Lisp (historically, LISP) is a family of computer programming languages with a long history and a distinctive, fully parenthesized prefix notation.
Mercury is a functional logic programming language made for real-world uses.
Miranda is a lazy, 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.
ML (Meta Language) is a general-purpose functional programming language.
In functional programming, a monad is a design pattern that defines how functions, actions, inputs, and outputs can be used together to build generic types, with the following organization.
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.
OCaml, originally named Objective Caml, is the main implementation of the programming language Caml, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez and others in 1996.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).
In programming languages and type theory, polymorphism (from Greek πολύς, polys, "many, much" and μορφή, morphē, "form, shape") is the provision of a single interface to entities of different types.
A programming language is a formal language that specifies a set of instructions that can be used to produce various kinds of output.
Programming paradigms are a way to classify programming languages based on their features.
Pure, successor to the equational language Q, is a dynamically typed, functional programming language based on term rewriting.
In computer science, purely functional programming usually designates a programming paradigm—a style of building the structure and elements of computer programs—that treats all computation as the evaluation of mathematical functions.
Q is a programming language for array processing, developed by Arthur Whitney.
Quantum programming is the process of assembling sequences of instructions, called quantum programs, that are capable of running on a quantum computer.
Referential transparency and referential opacity are properties of parts of computer programs.
Scala is a general-purpose programming language providing support for functional programming and a strong static type system.
Scheme is a programming language that supports multiple paradigms, including functional programming and imperative programming, and is one of the two main dialects of Lisp.
In computer programming, the scope of a name binding – an association of a name to an entity, such as a variable – is the region of a computer program where the binding is valid: where the name can be used to refer to the entity.
The SECD machine is a highly influential (See: #Landin's contribution) virtual machine and abstract machine intended as a target for functional programming language compilers.
In mathematical logic, a sequent is a very general kind of conditional assertion.
Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology.
In computer science, a function or expression is said to have a side effect if it modifies some state outside its scope or has an observable interaction with its calling functions or the outside world besides returning a value.
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.
SISAL ("Streams and Iteration in a Single Assignment Language") is a general-purpose single assignment functional programming language with strict semantics, implicit parallelism, and efficient array handling.
The SKI combinator calculus is a combinatory logic, a computational system that may be perceived as a reduced version of the untyped lambda calculus.
Speculative execution is an optimization technique where a computer system performs some task that may not be needed.
Standard ML (SML; "Standard Meta Language") is a general-purpose, modular, functional programming language with compile-time type checking and type inference.
A strict programming language is a programming language which employs a strict programming paradigm, allowing only strict functions (functions whose parameters must be evaluated completely before they may be called) may be defined by the user.
Template Haskell is an experimental language extension to the Haskell programming language implemented in the Glasgow Haskell Compiler (version 6 and later).
In theoretical computer science, a transition system is a concept used in the study of computation.
Type inference refers to the automatic detection of the data type of an expression in a programming language.
In computer science, a type signature or type annotation defines the inputs and outputs for a function, subroutine or method.
In type theory and programming languages, a type variable is a mathematical variable ranging over types.
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction.
In mathematics, specifically in category theory, the Yoneda lemma is an abstract result on functors of the type morphisms into a fixed object.