
Programming language theory (PLT) is a branch of
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
that deals with the design, implementation, analysis, characterization, and classification of
formal language
In logic, mathematics, computer science, and linguistics, a formal language is a set of strings whose symbols are taken from a set called "alphabet".
The alphabet of a formal language consists of symbols that concatenate into strings (also c ...
s known as
programming language
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
s. Programming language theory is closely related to other fields including
linguistics
Linguistics is the scientific study of language. The areas of linguistic analysis are syntax (rules governing the structure of sentences), semantics (meaning), Morphology (linguistics), morphology (structure of words), phonetics (speech sounds ...
,
mathematics
Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
, and
software engineering
Software engineering is a branch of both computer science and engineering focused on designing, developing, testing, and maintaining Application software, software applications. It involves applying engineering design process, engineering principl ...
.
History
In some ways, the history of programming language theory predates even the development of programming languages. The
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
, developed by
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American computer scientist, mathematician, logician, and philosopher who made major contributions to mathematical logic and the foundations of theoretical computer science. He is bes ...
and
Stephen Cole Kleene in the 1930s, is considered by some to be the world's first programming language, even though it was intended to ''
model
A model is an informative representation of an object, person, or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin , .
Models can be divided in ...
'' computation rather than being a means for programmers to ''
describe''
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
s to a computer system. Many modern
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...
languages have been described as providing a "thin veneer" over the lambda calculus, and many are described easily in terms of it.
The first programming language to be invented was
Plankalkül, which was designed by
Konrad Zuse
Konrad Ernst Otto Zuse (; ; 22 June 1910 – 18 December 1995) was a German civil engineer, List of pioneers in computer science, pioneering computer scientist, inventor and businessman. His greatest achievement was the world's first programm ...
in the 1940s, but not publicly known until 1972, and not implemented until 1998. The first widely known and successful
high-level programming language
A high-level programming language is a programming language with strong Abstraction (computer science), abstraction from the details of the computer. In contrast to low-level programming languages, it may use natural language ''elements'', be ea ...
was
FORTRAN (for Formula Translation), developed from 1954 to 1957 by a team of
IBM
International Business Machines Corporation (using the trademark IBM), nicknamed Big Blue, is an American Multinational corporation, multinational technology company headquartered in Armonk, New York, and present in over 175 countries. It is ...
researchers led by
John Backus. The success of FORTRAN led to the formation of a committee of scientists to develop a "universal" computer language; the result of their effort was
ALGOL 58. Separately,
John McCarthy of
Massachusetts Institute of Technology
The Massachusetts Institute of Technology (MIT) is a Private university, private research university in Cambridge, Massachusetts, United States. Established in 1861, MIT has played a significant role in the development of many areas of moder ...
(MIT) developed
Lisp
Lisp (historically LISP, an abbreviation of "list processing") is a family of programming languages with a long history and a distinctive, fully parenthesized Polish notation#Explanation, prefix notation.
Originally specified in the late 1950s, ...
, the first language with origins in academia to be successful. With the success of these initial efforts, programming languages became an active topic of research in the 1960s and beyond.
Timeline
Some other key events in the history of programming language theory since then:
; 1950s
*
Noam Chomsky
Avram Noam Chomsky (born December 7, 1928) is an American professor and public intellectual known for his work in linguistics, political activism, and social criticism. Sometimes called "the father of modern linguistics", Chomsky is also a ...
developed the
Chomsky hierarchy
The Chomsky hierarchy in the fields of formal language theory, computer science, and linguistics, is a containment hierarchy of classes of formal grammars. A formal grammar describes how to form strings from a formal language's alphabet that are v ...
in the field of linguistics, a discovery which has directly impacted programming language theory and other branches of computer science.
; 1960s
* In 1962, the
Simula
Simula is the name of two simulation programming languages, Simula I and Simula 67, developed in the 1960s at the Norwegian Computing Center in Oslo, by Ole-Johan Dahl and Kristen Nygaard. Syntactically, it is an approximate superset of AL ...
language was developed by
Ole-Johan Dahl
Ole-Johan Dahl (12 October 1931 – 29 June 2002) was a Norwegian computer scientist. Dahl was a professor of computer science at the University of Oslo and is considered to be one of the fathers of Simula and object-oriented programming along wi ...
and
Kristen Nygaard
Kristen Nygaard (27 August 1926 – 10 August 2002) was a Norwegian computer scientist, programming language pioneer, and politician. Internationally, Nygaard is acknowledged as the co-inventor of object-oriented programming and the programming ...
; it is widely considered to be the first example of an
object-oriented programming
Object-oriented programming (OOP) is a programming paradigm based on the concept of '' objects''. Objects can contain data (called fields, attributes or properties) and have actions they can perform (called procedures or methods and impl ...
language; Simula also introduced the concept of
coroutine
Coroutines are computer program components that allow execution to be suspended and resumed, generalizing subroutines for cooperative multitasking. Coroutines are well-suited for implementing familiar program components such as cooperative task ...
s.
* In 1964,
Peter Landin is the first to realize Church's lambda calculus can be used to model programming languages. He introduces the
SECD machine which "interprets" lambda expressions.
* In 1965, Landin introduces the
J operator, essentially a form of
continuation
In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements ( reifies) the program control state, i.e. the continuation is a data structure that represents the computat ...
.
* In 1966, Landin introduces
ISWIM, an abstract computer
programming language
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
in his article ''The Next 700 Programming Languages''. It is influential in the design of languages leading to the
Haskell
Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
language.
* In 1966,
Corrado Böhm
Corrado Böhm (17 January 1923 – 23 October 2017) was an Italian computer scientist and Professor Emeritus at the Sapienza University of Rome, University of Rome "La Sapienza", known especially for his contributions to the theory of structured ...
introduced the language CUCH (Curry-Church).
* In 1967,
Christopher Strachey
Christopher S. Strachey (; 16 November 1916 – 18 May 1975) was a British computer scientist. He was one of the founders of denotational semantics, and a pioneer in programming language design and computer time-sharing.F. J. Corbató, et al., T ...
publishes his influential set of lecture notes ''
Fundamental Concepts in Programming Languages
''Fundamental Concepts in Programming Languages'' were an influential set of lecture notes written by Christopher Strachey for the International Summer School in Computer Programming at Copenhagen in August, 1967. It introduced much programming ...
'', introducing the terminology ''
R-values, L-values'', ''
parametric polymorphism'', and ''
ad hoc polymorphism''.
* In 1969,
J. Roger Hindley publishes ''The Principal Type-Scheme of an Object in Combinatory Logic'', later generalized into the
Hindley–Milner type inference
Type inference, sometimes called type reconstruction, refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some bran ...
algorithm.
* In 1969,
Tony Hoare
Sir Charles Antony Richard Hoare (; born 11 January 1934), also known as C. A. R. Hoare, is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and ...
introduces the
Hoare logic
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and l ...
, a form of
axiomatic semantics
Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic.
Axiomatic semantics define the meaning of a command in a program by describing its effect on ...
.
* In 1969,
William Alvin Howard observed that a "high-level"
proof system, referred to as
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. This contrasts with Hilbert-style systems, which instead use ...
, can be directly interpreted in its
intuitionistic version as a typed variant of the
model of computation known as
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
. This became known as the
Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-p ...
.
; 1970s
* In 1970,
Dana Scott first publishes his work on
denotational semantics
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...
.
* In 1972,
logic programming
Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
and
Prolog
Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics.
Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...
were developed thus allowing computer programs to be expressed as mathematical logic.
* A team of scientists at
Xerox PARC led by
Alan Kay
Alan Curtis Kay (born May 17, 1940) published by the Association for Computing Machinery 2012 is an American computer scientist who pioneered work on object-oriented programming and windowing graphical user interface (GUI) design. At Xerox ...
develop
Smalltalk
Smalltalk is a purely object oriented programming language (OOP) that was originally created in the 1970s for educational use, specifically for constructionist learning, but later found use in business. It was created at Xerox PARC by Learni ...
, an object-oriented language widely known for its innovative development environment.
* In 1974,
John C. Reynolds discovers
System F. It had already been discovered in 1971 by the mathematical logician
Jean-Yves Girard.
* From 1975,
Gerald Jay Sussman and
Guy Steele
Guy Lewis Steele Jr. (; born October 2, 1954) is an American computer scientist who has played an important role in designing and documenting several computer programming languages and technical standards.
Biography
Steele was born in Missouri ...
develop the
Scheme language, a Lisp dialect incorporating
lexical scoping, a unified namespace, and elements from the
actor model
The actor model in computer science is a mathematical model of concurrent computation that treats an ''actor'' as the basic building block of concurrent computation. In response to a message it receives, an actor can: make local decisions, create ...
including first-class
continuation
In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements ( reifies) the program control state, i.e. the continuation is a data structure that represents the computat ...
s.
* Backus, at the 1977
Turing Award
The ACM A. M. Turing Award is an annual prize given by the Association for Computing Machinery (ACM) for contributions of lasting and major technical importance to computer science. It is generally recognized as the highest distinction in the fi ...
lecture, assailed the current state of industrial languages and proposed a new class of programming languages now known as
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.
In his 1977 Turin ...
languages.
* In 1977,
Gordon Plotkin introduces
Programming Computable Functions, an abstract typed functional language.
* In 1978,
Robin Milner introduces the
Hindley–Milner type system inference algorithm for
ML language.
Type theory
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
became applied as a discipline to programming languages, this application has led to great advances in type theory over the years.
; 1980s
* In 1981,
Gordon Plotkin publishes his paper on
structured operational semantics.
* In 1988,
Gilles Kahn published his paper on
natural semantics.
* There emerged
process calculi, such as the
Calculus of Communicating Systems of
Robin Milner, and the
Communicating sequential processes model of
C. A. R. Hoare, as well as similar models of concurrency such as the
actor model
The actor model in computer science is a mathematical model of concurrent computation that treats an ''actor'' as the basic building block of concurrent computation. In response to a message it receives, an actor can: make local decisions, create ...
of
Carl Hewitt.
* In 1985, the release of
Miranda sparks an academic interest in lazy-evaluated
purely functional programming
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 function (mathematics), mathematic ...
languages. A committee was formed to define an open standard resulting in the release of the Haskell 1.0 standard in 1990.
*
Bertrand Meyer
Bertrand Meyer (; ; born 21 November 1950) is a French academic, author, and consultant in the field of computer languages. He created the Eiffel programming language and the concept of design by contract.
Education and academic career
Meyer ...
created the methodology ''
design by contract'' and incorporated it into the
Eiffel language.
; 1990s
*
Gregor Kiczales, Jim Des Rivieres and
Daniel G. Bobrow published the book ''
The Art of the Metaobject Protocol''.
*
Eugenio Moggi and
Philip Wadler introduced the use of
monads for structuring programs written in
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...
languages.
Sub-disciplines and related fields
There are several fields of study that either lie within programming language theory, or which have a profound influence on it; many of these have considerable overlap. In addition, PLT makes use of many other branches of
mathematics
Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
, including
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ex ...
,
category theory
Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...
, and
set theory
Set theory is the branch of mathematical logic that studies Set (mathematics), sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory – as a branch of mathema ...
.
Formal semantics
Formal semantics is the formal specification of the behaviour of computer programs and programming languages. Three common approaches to describe the semantics or "meaning" of a computer program are
denotational semantics
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...
,
operational semantics
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 exec ...
and
axiomatic semantics
Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic.
Axiomatic semantics define the meaning of a command in a program by describing its effect on ...
.
Type theory
Type theory is the study of
type system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
s; which are "a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute".
[Benjamin C. Pierce. 2002]
Types and Programming Languages
MIT Press, Cambridge, Massachusetts, USA. Many programming languages are distinguished by the characteristics of their type systems.
Program analysis and transformation
Program analysis is the general problem of examining a program and determining key characteristics (such as the absence of classes of
program errors). Program transformation is the process of transforming a program in one form (language) to another form.
Comparative programming language analysis
Comparative programming language analysis seeks to classify languages into different types based on their characteristics; broad categories of languages are often known as
programming paradigm
A programming paradigm is a relatively high-level way to conceptualize and structure the implementation of a computer program. A programming language can be classified as supporting one or more paradigms.
Paradigms are separated along and descri ...
s.
Generic and metaprogramming
Metaprogramming
Metaprogramming is a computer programming technique in which computer programs have the ability to treat other programs as their data. It means that a program can be designed to read, generate, analyse, or transform other programs, and even modi ...
is the generation of higher-order programs which, when executed, produce programs (possibly in a different language, or in a subset of the original language) as a result.
Domain-specific languages
Domain-specific languages are those constructed to efficiently solve problems in a given domain, or part of such.
Compiler construction
Compiler
In computing, a compiler is a computer program that Translator (computing), translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primaril ...
theory is the theory of writing ''compilers'' (or more generally, ''translators''); programs that translate a program written in one language into another form. The actions of a compiler are traditionally broken up into ''syntax analysis'' (
scanning and
parsing
Parsing, syntax analysis, or syntactic analysis is a process of analyzing a String (computer science), string of Symbol (formal), symbols, either in natural language, computer languages or data structures, conforming to the rules of a formal gramm ...
), ''semantic analysis'' (determining what a program should do), ''
optimization
Mathematical optimization (alternatively spelled ''optimisation'') or mathematical programming is the selection of a best element, with regard to some criteria, from some set of available alternatives. It is generally divided into two subfiel ...
'' (improving the performance of a program as indicated by some metric; typically execution speed) and ''
code generation'' (generation and output of an equivalent program in some target language; often the
instruction set architecture
In computer science, an instruction set architecture (ISA) is an abstract model that generally defines how software controls the CPU in a computer or a family of computers. A device or program that executes instructions described by that ISA, ...
of a
central processing unit
A central processing unit (CPU), also called a central processor, main processor, or just processor, is the primary Processor (computing), processor in a given computer. Its electronic circuitry executes Instruction (computing), instructions ...
(CPU)).
Run-time systems
Run-time systems refer to the development of programming language
runtime environment
In computer programming, a runtime system or runtime environment is a sub-system that exists in the computer where a program is created, as well as in the computers where the program is intended to be run. The name comes from the compile time ...
s and their components, including
virtual machine
In computing, a virtual machine (VM) is the virtualization or emulator, emulation of a computer system. Virtual machines are based on computer architectures and provide the functionality of a physical computer. Their implementations may involve ...
s,
garbage collection, and
foreign function interfaces.
Journals, publications, and conferences
Conferences are the primary venue for presenting research in programming languages. The most well known conferences include the ''
Symposium on Principles of Programming Languages'' (POPL), ''
Programming Language Design and Implementation'' (PLDI), the ''
International Conference on Functional Programming'' (ICFP), the international conference on ''Object-Oriented Programming, Systems, Languages & Applications'' (
OOPSLA) and the ''
International Conference on Architectural Support for Programming Languages and Operating Systems'' (ASPLOS).
Notable journals that publish PLT research include the ''
ACM Transactions on Programming Languages and Systems'' (TOPLAS), ''
Journal of Functional Programming'' (JFP), ''
Journal of Functional and Logic Programming'', and ''
Higher-Order and Symbolic Computation''.
See also
*
SIGPLAN
SIGPLAN is the Association for Computing Machinery's Special Interest Group (SIG) on programming languages. This SIG explores programming language concepts and tools, focusing on design, implementation, practice, and theory. Its members are progra ...
*
Very high-level programming language
References
Further reading
*
Abadi, Martín and
Cardelli, Luca. ''A Theory of Objects''. Springer-Verlag.
*
Michael J. C. Gordon. ''Programming Language Theory and Its Implementation''. Prentice Hall.
* Gunter, Carl and
Mitchell, John C. (eds.). ''Theoretical Aspects of Object Oriented Programming Languages: Types, Semantics, and Language Design''. MIT Press.
*
Harper, Robert.
Practical Foundations for Programming Languages'. Draft version.
*
Knuth, Donald E. (2003).
Selected Papers on Computer Languages'. Stanford, California: Center for the Study of Language and Information.
*
Mitchell, John C. ''Foundations for Programming Languages''.
*
Mitchell, John C. ''Introduction to Programming Language Theory''.
*
O'Hearn, Peter. W. and Tennent, Robert. D. (1997).
ALGOL-like Languages'. Progress in Theoretical Computer Science. Birkhauser, Boston.
*
Pierce, Benjamin C. (2002).
Types and Programming Languages'. MIT Press.
* Pierce, Benjamin C. ''Advanced Topics in Types and Programming Languages''.
* Pierce, Benjamin C. ''et al.'' (2010).
Software Foundations'.
External links
{{Commons category
Lambda the Ultimate a community weblog for professional discussion and repository of documents on programming language theory.
Great Works in Programming Languages Collected by
Benjamin C. Pierce (
University of Pennsylvania
The University of Pennsylvania (Penn or UPenn) is a Private university, private Ivy League research university in Philadelphia, Pennsylvania, United States. One of nine colonial colleges, it was chartered in 1755 through the efforts of f ...
).
Classic Papers in Programming Languages and Logic Collected by Karl Crary (
Carnegie Mellon University
Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania, United States. The institution was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became the Carnegie Institu ...
).
Programming Language Research Directory by Mark Leone.
λ-Calculus: Then & Nowby
Dana S. Scott for the ACM Turing Centenary Celebration
Grand Challenges in Programming Languages Panel session at
POPL 2009.