Theories of Programming LanguagesFirst published in 1998, this textbook is a broad but rigourous survey of the theoretical basis for the design, definition and implementation of programming languages and of systems for specifying and proving programme behaviour. Both imperative and functional programming are covered, as well as the ways of integrating these aspects into more general languages. Recognising a unity of technique beneath the diversity of research in programming languages, the author presents an integrated treatment of the basic principles of the subject. He identifies the relatively small number of concepts, such as compositional semantics, binding structure, domains, transition systems and inference rules, that serve as the foundation of the field. Assuming only knowledge of elementary programming and mathematics, this text is perfect for advanced undergraduate and beginning graduate courses in programming language theory and also will appeal to researchers and professionals in designing or implementing computer languages. |
Contents
11 | |
The SimpleImperative Language | |
4 Lists | |
Arrays | |
The Lambda Calculus | |
Functional | |
Continuations in a Functional | |
Iswimlike Languages | |
NormalOrder | |
The Simple Type System | |
Subtypes and Intersection Types 16 1 Inference Rules forSubtyping 16 2 Named Products and Sums | |
Polymorphism | |
Failure InputOutput | |
Powerdomains | |
SharedVariable Concurrency | |
Communicating Sequential | |
Module Specification 18 1 Type Definitions | |
Mathematical Background | |
Functions A 4 Relations and Functions Between Sets | |
Other editions - View all
Common terms and phrases
abstract syntax application argument array variable assignment command called canonical form chain Chapter CN SEM EQ computation construction constructors continuation semantics continuous function defined definition denotational semantics described direct semantics domain DR SEM EQ eager evaluation element error example execution extend fib(k final finite sequence formal function f FV comm give guarded commands induction inference rules infinite initial injections input inputoutput integer integer expression inthe introduce isomorphism lambda calculus least fixedpoint maps metalanguage metavariable monotone function newvar nondeterminism nonterminal nonterminal configuration occur free ofthe operational semantics operations output partial correctness phrases pointwise ordering predicate logic predomain premisses processes programming languages proof Proposition prove recursive reduction sequence renaming result satisfies semantic equation semantic function SEMEQ Sequential Composition simple imperative language SP RULE subphrase subscript substitution Suppose terminal configuration theorem TR RULE transition relation transition semantics valid Variable Declaration wewill zero