natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The book
Practical Foundations for Programming Languages
Cambridge University Press (2016)
lays the foundations of the theory of programming languages in terms of type theory. In over 500 pages, the author formally specifies and step-by-step extends established type systems and reasons about type safety and operational semantics (not so much about dependent types and categorical semantics). The book also contains a discussion of formal logic in type theory and features of variants of the Algol
programming language, in particular.
[p. xvii:] Types are the central organizing principle of the theory of programming languages. Language features are manifestations of type structure. The syntax of a language is governed by the constructs that define its types, and its semantics is determined by the interactions among those constructs. The soundness of a language design—the absence of ill-defined programs—follows naturally. The purpose of this book is to explain this remark.
The preview of the second edition (2016) is available as a pdf. A description of the changes is here.
Carl A. Gunter: The semantics of types in programming languages, in: Handbook of Logic in Computer Science Vol 3: Semantic Structures, Oxford University Press (1995) [pdf]
Practical Foundations of Mathematics
(web)
William Lawvere, Robert Rosebrugh,
Cambridge UP 2003 (book homepage, GoogleBooks, pdf)
Last revised on December 30, 2022 at 07:09:43. See the history of this page for a list of all contributions to it.