HOME

TheInfoList



OR:

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 & Now
by Dana S. Scott for the ACM Turing Centenary Celebration
Grand Challenges in Programming Languages
Panel session at POPL 2009.