In type theory, a typing rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well-typed and what type expressions have. A prototypical example of the use of typing rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.

Notation

Typing rules specify the structure of a typing relation that relates syntactic terms to their types. Adapting a declarative rule system to a decidable algorithm requires the production of a separate, algorithmic system that can be proven to specify the same typing relation.

See also

  • Judgment (mathematical logic)
  • Type system
  • Type theory
  • Curry–Howard correspondence
  • Sequent calculus

References

Further reading

<!-- I attempted to use this template but got unsure if it was the proper one so I wrote it manually down in the next bullet point after this comment.

  • -->
  • Cardelli, Luca (June 2004). Type Systems, 41 pages. Computer Science Handbook, 2nd Edition, Ch. 97. Edited by Allen B. Tucker. ISBN 9780429209390. Retrieved 5 January 2025.