Back to Notations

for Type Judgment

A formal statement asserting that a term has a certain type in a given context

Syntax Forms

Typst $Gamma tack.r e : tau$
LaTeX \Gamma \vdash e : \tau

Semantic Information

Also Known As
  • • typing relation
  • • type assignment
Categories
type theory PLT

Academic Usage

Types and Programming Languages

Benjamin C. Pierce • 2002

Context: Introduced in Chapter 3 as the fundamental judgment of type systems

Referenced on page 32

Primary Definition