programming language theory the lowercase greek letter lambda is an unofficial symbol of the field of programming language theory this usage derives from the lambda calculus a model of computation introduced by alonzo church in the 1930s and widely used by programming language researchers it graces the cover of the classic text structure and interpretation of computer programs and the title of the socalled lambda papers written by gerald jay sussman and guy steele the developers of the scheme programming language 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 wellrecognized 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 history 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 worlds 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 and many are easily described in terms of it the first programming language to be invented was plankalkl 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 highlevel 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 some other key events in the history of programming language theory since then 1950s 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 1960s the simula language was developed by olejohan dahl and kristen nygaard it is widely considered to be the first example of an objectoriented programming language simula also introduced the concept of coroutines in 1964 peter landin is the first to realize churchs 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 bhm introduced the programming language cuch currychurch in 1967 christopher strachey publishes his influential set of lecture notes fundamental concepts in programming languages introducing the terminology rvalues lvalues parametric polymorphism and ad hoc polymorphism in 1969 j roger hindley publishes the principal typescheme of an object in combinatory logic later generalized into the hindleymilner type inference algorithm in 1969 tony hoare introduces the hoare logic a form of axiomatic semantics in 1969 william alvin howard observed that a highlevel 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 curryhoward correspondence 1970s 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 objectoriented 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 jeanyves 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 firstclass 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 functionlevel programming languages in 1977 gordon plotkin introduces programming computable functions an abstract typed functional language in 1978 robin milner introduces the hindleymilner 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 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 of carl hewitt in 1985 the release of miranda sparks an academic interest in lazyevaluated pure functional programming languages a committee was formed to define an open standard resulting in the release of the haskell 10 standard in 1990 bertrand meyer created the methodology design by contract and incorporated it into the eiffel programming 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 languages subdisciplines and related fields 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 formal semantics of programming languages 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 type theory 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 many programming languages are distinguished by the characteristics of their type systems program analysis and transformation program analysis and program 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 programming languages into different types based on their characteristics broad categories of programming languages are often known as programming paradigms generic and metaprogramming metaprogramming is the generation of higherorder programs which when executed produce programs possibly in a different language or in a subset of the original language as a result domainspecific languages domainspecific languages are languages constructed to efficiently solve problems of a particular part of domain compiler construction compiler construction 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 runtime systems refers to the development of programming language runtime environments and their components including virtual machines 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 conference on programming language design and implementation pldi the international conference on functional programming icfp and the international conference on object oriented programming systems languages and applications oopsla 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 higherorder and symbolic computation sigplan timeline of programming languages very highlevel programming language see also programming language further reading and semantics of programming languages further reading abadi martn and cardelli luca a theory of objects springerverlag 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 ohearn peter w and tennent robert d 1997 algollike 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 