WikiMili The Free Encyclopedia

* Types and Programming Languages*, ISBN 0-262-16209-1, is a book by Benjamin C. Pierce on type systems published in 2002.

The **International Standard Book Number** (**ISBN**) is a numeric commercial book identifier which is intended to be unique. Publishers purchase ISBNs from an affiliate of the International ISBN Agency.

As a physical object, a **book** is a stack of usually rectangular pages oriented with one edge tied, sewn, or otherwise fixed together and then bound to the flexible spine of a protective cover of heavier, relatively inflexible material. The technical term for this physical arrangement is *codex*. In the history of hand-held physical supports for extended written compositions or records, the codex replaces its immediate predecessor, the scroll. A single sheet in a codex is a leaf, and each side of a leaf is a page.

A review by Frank Pfenning called it "probably the single most important book in the area of programming languages in recent years."^{ [1] }

**Frank Pfenning** is a professor of computer science, adjunct professor in the department of philosophy, and head of the Computer Science Department at Carnegie Mellon University. He received his Ph.D. from the Carnegie Mellon University Department of Mathematics in 1987, for his dissertation entitled *Proof Transformations in Higher-Order Logic*. He was a student of Peter B. Andrews.

**Programming paradigms** are a way to classify programming languages based on their features. Languages can be classified into multiple paradigms.

In logic, a **logical framework** provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, **LF**. Several more recent proof tools like Isabelle are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.

**Kenneth Jon Barwise** was an American mathematician, philosopher and logician who proposed some fundamental revisions to the way that logic is understood and used.

In computer science and mathematical logic, a **proof assistant** or **interactive theorem prover** is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

**Benjamin Crawford Pierce** is the Henry Salvatori Professor of computer science at the University of Pennsylvania. Pierce joined Penn in 1998 from Indiana University and held research positions at the University of Cambridge and the University of Edinburgh. He received his Ph.D. from Carnegie Mellon University in 1991. His research includes work on programming languages, static type systems, distributed programming, mobile agents, and process calculi.

**Dependent ML** is an experimental functional programming language proposed by Hongwei Xi and Frank Pfenning. Dependent ML extends ML by a restricted notion of dependent types: types may be dependent on static indices of type Nat. Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions.

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.

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

In type theory, a theory within mathematical logic, the **bottom type** is the type that has no values. It is also called the **zero** or **empty** type, and is sometimes denoted with falsum (⊥).

The **top type** in the type theory of mathematics, logic, and computer science, commonly abbreviated as **top** or by the *down tack* symbol (⊤), is the *universal* type, sometimes called the *universal supertype* as all other types in any given type system are subtypes of top. In most cases it is the type which contains every possible object in the type system of interest. It is in contrast with the bottom type, or the *universal subtype*, which every other type is supertype of and in most cases it is the type that contains no members at all.

**Peter Bruce Andrews** (born 1937) is an American mathematician and Professor of Mathematics, Emeritus at Carnegie Mellon University in Pittsburgh, Pennsylvania, and the creator of the mathematical logic Q_{0}. He received his Ph.D. from Princeton University in 1964 under the tutelage of Alonzo Church. He received the Herbrand Award in 2003. His research group designed the TPS automated theorem prover. A subsystem ETPS (Educational Theorem Proving System) of TPS is used to help students learn logic by interactively constructing natural deduction proofs.

The **ACM–IEEE Symposium on Logic in Computer Science** (**LICS**) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

In mathematical logic, a **judgment** or **assertion** is a statement or enunciation in the metalanguage. For example, typical judgments in first-order logic would be *that a string is a well-formed formula*, or *that a proposition is true*. Similarly, a judgment may assert the occurrence of a free variable in an expression of the object language, or the provability of a proposition. In general, a judgment may be any inductively definable assertion in the metatheory.

In the branch of mathematical logic known as type theory, **System F _{<:}**, pronounced "F-sub", is an extension of system F with subtyping. System F

In type theory, a **refinement type** is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as . Refinement types are thus related to behavioral subtyping.

**Robert Ian Goldblatt** is a mathematical logician who is Emeritus Professor in the School of Mathematics and Statistics at Victoria University, Wellington, New Zealand. His most popular books are *Logics of Time and Computation* and *Topoi: the Categorial Analysis of Logic*. He has also written a graduate level textbook on hyperreal numbers which is an introduction to nonstandard analysis.

* 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 language terminology still in use today, including "R-value" and "L-value", "ad hoc polymorphism", "parametric polymorphism", and "referential transparency".

**Jean-Pierre Jouannaud** is a French computer scientist, known for his work in the area of term rewriting.

**Jean Henri Gallier** is a researcher in computational logic at the University of Pennsylvania, where he holds appointments in the Computer and Information Science Department and the Department of Mathematics.

- ↑ Pfenning, Frank (June 2004). "review of
*Types and Programming Languages*by Benjamin C. Pierce".*The Bulletin of Symbolic Logic*. Association for Symbolic Logic.**10**(2): 213–214. doi:10.1017/s1079898600003954. JSTOR 3176763.

This article about a computer book or series of books is a stub. You can help Wikipedia by expanding it. |

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.