WikiMili The Free Encyclopedia

This article includes a list of references, but its sources remain unclear because it has insufficient inline citations .(October 2015) (Learn how and when to remove this template message) |

**Programming language theory** (**PLT**) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting mathematics, software engineering, linguistics and even cognitive science. It is a well-recognized branch of computer science, and an active research area, with results published in numerous journals dedicated to PLT, as well as in general computer science and engineering publications.

**Computer science** is the study of processes that interact with data and that can be represented as data in the form of programs. It enables the use of algorithms to manipulate, store, and communicate digital information. A computer scientist studies the theory of computation and the practice of designing software systems.

A **programming language** is a formal language, which comprises a set of instructions that produce various kinds of output. Programming languages are used in computer programming to implement algorithms.

**Mathematics** includes the study of such topics as quantity, structure (algebra), space (geometry), and change. It has no generally accepted definition.

- History
- 1950s
- 1960s
- 1970s
- 1980s
- 1990s
- Sub-disciplines and related fields
- Formal semantics
- Type theory
- Program analysis and transformation
- Comparative programming language analysis
- Generic and metaprogramming
- Domain-specific languages
- Compiler construction
- Run-time systems
- Journals, publications, and conferences
- See also
- References
- Further reading
- External links

In some ways, the history of programming language theory predates even the development of programming languages themselves. The lambda calculus, developed by Alonzo Church 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* computation rather than being a means for programmers to *describe* algorithms to a computer system. Many modern functional programming languages have been described as providing a "thin veneer" over the lambda calculus,^{ [1] } and many are easily described in terms of it.

**Lambda calculus** is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was first introduced by mathematician Alonzo Church in the 1930s as part of his research of the foundations of mathematics.

**Alonzo Church** was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, proving the undecidability of the Entscheidungsproblem, Frege–Church ontology, and the Church–Rosser theorem. He also worked on philosophy of language.

**Stephen Cole Kleene** was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of mathematical logic known as recursion theory, which subsequently helped to provide the foundations of theoretical computer science. Kleene's work grounds the study of computable functions. A number of mathematical concepts are named after him: Kleene hierarchy, Kleene algebra, the Kleene star, Kleene's recursion theorem and the Kleene fixpoint theorem. He also invented regular expressions, and made significant contributions to the foundations of mathematical intuitionism.

The first programming language to be invented was Plankalkül, which was designed by Konrad Zuse in the 1940s, but not publicly known until 1972 (and not implemented until 1998). The first widely known and successful high-level programming language was Fortran, developed from 1954 to 1957 by a team of IBM 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 MIT developed the Lisp programming language (based on the lambda calculus), 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.

**Plankalkül** is a programming language designed for engineering purposes by Konrad Zuse between 1942 and 1945. It was the first high-level programming language to be designed for a computer.

**Konrad Zuse** was a German civil engineer, computer scientist, inventor, businessman and computer pioneer. His greatest achievement was the world's first programmable computer; the functional program-controlled Turing-complete Z3 became operational in May 1941. Thanks to this machine and its predecessors, Zuse has often been regarded as the inventor of the modern computer.

In computer science, a **high-level programming language** is a programming language with strong abstraction from the details of the computer. In contrast to low-level programming languages, it may use natural language *elements*, be easier to use, or may automate significant areas of computing systems, making the process of developing a program simpler and more understandable than when using a lower-level language. The amount of abstraction provided defines how "high-level" a programming language is.

Some other key events in the history of programming language theory since then:

- Noam Chomsky developed the Chomsky hierarchy in the field of linguistics; a discovery which has directly impacted programming language theory and other branches of computer science.

**Avram Noam Chomsky** is an American linguist, philosopher, cognitive scientist, historian, social critic, and political activist. Sometimes called "the father of modern linguistics", Chomsky is also a major figure in analytic philosophy and one of the founders of the field of cognitive science. He holds a joint appointment as Institute Professor Emeritus at the Massachusetts Institute of Technology (MIT) and laureate professor at the University of Arizona, and is the author of more than 100 books on topics such as linguistics, war, politics, and mass media. Ideologically, he aligns with anarcho-syndicalism and libertarian socialism.

In the formal languages of computer science and linguistics, the **Chomsky hierarchy** is a containment hierarchy of classes of formal grammars.

**Linguistics** is the scientific study of language. It involves analysing language form, language meaning, and language in context. The earliest activities in the documentation and description of language have been attributed to the 6th-century-BC Indian grammarian Pāṇini who wrote a formal description of the Sanskrit language in his * Aṣṭādhyāyī*.

- The Simula language was developed by Ole-Johan Dahl and Kristen Nygaard; it is widely considered to be the first example of an object-oriented programming language; Simula also introduced the concept of coroutines.
- 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 1966, Landin introduces ISWIM, an abstract computer programming language in his article
*The Next 700 Programming Languages*. It is influential in the design of languages leading to the Haskell programming language. - In 1966, Corrado Böhm introduced the programming language CUCH (Curry-Church).
^{ [2] } - In 1967, Christopher Strachey publishes his influential set of lecture notes
*Fundamental Concepts in Programming Languages*, 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 algorithm. - In 1969, Tony Hoare introduces the Hoare logic, a form of axiomatic semantics.
- In 1969, William Alvin Howard observed that a "high-level" proof system, referred to as natural deduction, can be directly interpreted in its intuitionistic version as a typed variant of the model of computation known as lambda calculus. This became known as the Curry–Howard correspondence.

**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 a fairly faithful superset of ALGOL 60, also influenced by the design of Simscript.

**Ole-Johan Dahl** 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 with Kristen Nygaard.

**Kristen Nygaard** 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 language Simula with Ole-Johan Dahl in the 1960s. Nygaard and Dahl received the 2001 A. M. Turing Award for their contribution to computer science.

- In 1970, Dana Scott first publishes his work on denotational semantics.
- In 1972, logic programming and Prolog were developed thus allowing computer programs to be expressed as mathematical logic.
- A team of scientists at Xerox PARC led by Alan Kay develop Smalltalk, 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 develop the Scheme programming language, a Lisp dialect incorporating lexical scoping, a unified namespace, and elements from the actor model including first-class continuations.
- Backus, at the 1977 ACM Turing Award lecture, assailed the current state of industrial languages and proposed a new class of programming languages now known as function-level programming languages.
- In 1977, Gordon Plotkin introduces Programming Computable Functions, an abstract typed functional language.
- In 1978, Robin Milner introduces the Hindley–Milner type inference algorithm for the ML programming language. Type theory became applied as a discipline to programming languages, this application has led to tremendous advances in type theory over the years.

**Dana Stewart Scott** is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California. His research career involved computer science, mathematics, and philosophy. His work on automata theory earned him the ACM Turing Award in 1976, while his collaborative work with Christopher Strachey in the 1970s laid the foundations of modern approaches to the semantics of programming languages. He has worked also on modal logic, topology, and category theory.

In computer science, **denotational semantics** is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches provide formal semantics of programming languages including axiomatic semantics and operational semantics.

**Logic programming** is a type of programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, answer set programming (ASP) and Datalog. In all of these languages, rules are written in the form of *clauses*:

- 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 of Carl Hewitt.
- In 1985, the release of Miranda sparks an academic interest in lazy-evaluated pure functional programming languages. A committee was formed to define an open standard resulting in the release of the Haskell 1.0 standard in 1990.
- Bertrand Meyer created the methodology Design by contract and incorporated it into the Eiffel programming language.

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

There are several fields of study which 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, including computability theory, category theory, and set theory.

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, operational semantics and axiomatic semantics.

Type theory is the study of type systems; 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".^{ [3] } Many programming languages are distinguished by the characteristics of their type systems.

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 seeks to classify programming languages into different types based on their characteristics; broad categories of programming languages are often known as programming paradigms.

Metaprogramming 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 are languages constructed to efficiently solve problems of a particular part of domain.

Compiler theory is the theory of writing *compilers* (or more generally, *translators*); programs which 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), *semantic analysis* (determining what a program should do), * optimization * (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 of a CPU).

Runtime systems refers to the development of programming language runtime environments and their components, including virtual machines, garbage collection, and foreign function interfaces.

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 and 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 *.

In mathematics, logic, and computer science, a **type theory** is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

**Combinatory logic** is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and 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 languages. It is based on **combinators** which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions - and to remove any mention of variables - particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.

**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. The acronym stands for "**If you See What I Mean**".

In programming language theory and proof theory, the **Curry–Howard correspondence** is the direct relationship between computer programs and mathematical proofs.

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. From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and *untyped lambda calculus* a special case with only one type.

In programming language theory, **semantics** is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically valid strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically invalid strings, the result would be non-computation. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation.

**Categorical logic** is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970.

The **actor model** in computer science is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent computation. In response to a message that it receives, an actor can: make local decisions, create more actors, send more messages, and determine how to respond to the next message received. Actors may modify their own private state, but can only affect each other indirectly through messaging.

**Quantum programming** is the process of assembling sequences of instructions, called quantum programs, that are capable of running on a quantum computer. Quantum programming languages help express quantum algorithms using high-level constructs.

In computer science, the **Actor model** and **process calculi** are two closely related approaches to the modelling of concurrent digital computation. See Actor model and process calculi history.

In computer science, **Programming Computable Functions**, or **PCF**, is a typed functional language introduced by Gordon Plotkin in 1977, based on previous unpublished material by Dana Scott. It can be considered to be an extended version of the typed lambda calculus or a simplified version of modern typed functional languages such as ML or Haskell.

In programming languages and type theory, **parametric polymorphism** is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values *identically* without depending on their type. Such functions and data types are called **generic functions** and **generic datatypes** respectively and form the basis of generic programming.

The **Actor model** and **process calculi** share an interesting **history** and co-evolution.

**Harry George Mairson** is a theoretical computer scientist and Professor of Computer Science in the Volen National Center for Complex Systems at Brandeis University in Waltham, Massachusetts. His research is in the fields of logic in computer science, lambda calculus and functional programming, type theory and constructive mathematics, computational complexity theory, and algorithmics.

The **categorical abstract machine** (**CAM**) is a model of computation for programs that preserves the abilities of applicative, functional, or compositional style. It is based on the techniques of applicative computing.

**Applicative computing systems**, or **ACS** are the systems of object calculi founded on combinatory logic and lambda calculus. The only essential notion which is under consideration in these systems is the representation of object. In combinatory logic the only metaoperator is application in a sense of applying one object to other. In lambda calculus two metaoperators are used: application – the same as in combinatory logic, and functional abstraction which binds the only variable in one object.

**Carl Eddie Hewitt** is an American computer scientist who designed the Planner programming language for automated planning and the actor model of concurrent computation, which have been influential in the development of logic, functional and object-oriented programming. Planner was the first programming language based on procedural plans invoked using pattern-directed invocation from assertions and goals. The actor model influenced the development of the Scheme programming language, the π-calculus, and served as an inspiration for several other programming languages.

- ↑ http://www.c2.com/cgi/wiki?ModelsOfComputation
- ↑ C. Böhm and W. Gross (1996). Introduction to the CUCH. In E. R. Caianiello (ed.),
*Automata Theory*, p. 35-64/ - ↑ Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, Massachusetts, USA.

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

Wikimedia Commons has media related to . Programming language theory |

- 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).
- Classic Papers in Programming Languages and Logic. Collected by Karl Crary (Carnegie Mellon University).
- Programming Language Research. Directory by Mark Leone.
- Programming Language Theory Texts Online. At Utrecht University.
- λ-Calculus: Then & Now by Dana S. Scott for the ACM Turing Centenary Celebration
- Grand Challenges in Programming Languages. Panel session at POPL 2009.

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.