text:
Type theory

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.

Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that have been proposed as foundations are:

 * Typed λ-calculus of Alonzo Church
 * Intuitionistic type theory of Per Martin-Löf

Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions.

History
Type theory was created to avoid a paradox in a mathematical equation based on naive set theory and formal logic. Russell's paradox (first described in Gottlob Frege's The Foundations of Arithmetic) is that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908, Bertrand Russell proposed various solutions to this problem.

By 1908, Russell arrived at a ramified theory of types together with an axiom of reducibility, both of which appeared in Whitehead and Russell's Principia Mathematica published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of subtypes of that type, thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as Zermelo-Fraenkel set theory.

Type theory is particularly popular in conjunction with Alonzo Church's lambda calculus. One notable early example of type theory is Church's simply typed lambda calculus. Church's theory of types helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated that it could serve as a foundation of mathematics and it was referred to as a higher-order logic.

In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Coq, Lean, and other computer proof assistants. Type theory is an active area of research, one direction being the development of homotopy type theory.

Mathematical foundations
The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode all mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using homotopy type theory.

Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS). Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy).

Proof assistants
Much of the current research into type theory is driven by proof checkers, interactive proof assistants, and automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages:
 * LF is used by Twelf, often to define other type theories;
 * many type theories which fall under higher-order logic are used by the HOL family of provers and PVS;
 * computational type theory is used by NuPRL;
 * calculus of constructions and its derivatives are used by Coq, Matita, and Lean;
 * UTT (Luo's Unified Theory of dependent Types) is used by Agda which is both a programming language and proof assistant

Many type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory.

Programming languages
Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory. A prime example is Agda, a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system.

The programming language ML was developed for manipulating type theories (see LCF) and its own type system was heavily influenced by them.

Linguistics
Type theory is also widely used in formal theories of semantics of natural languages, especially Montague grammar and its descendants. In particular, categorial grammars and pregroup grammars extensively use type constructors to define the types (noun, verb, etc.) of words.

The most common construction takes the basic types $$e$$ and $$t$$ for individuals and truth-values, respectively, and defines the set of types recursively as follows:
 * if $$a$$ and $$b$$ are types, then so is $$\langle a,b\rangle$$;
 * nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type $$\langle a,b\rangle$$ is the type of functions from entities of type $$a$$ to entities of type $$b$$. Thus one has types like $$\langle e,t\rangle$$ which are interpreted as elements of the set of functions from entities to truth-values, i.e. indicator functions of sets of entities. An expression of type $$\langle\langle e,t\rangle,t\rangle$$ is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like  everybody or nobody (Montague 1973, Barwise and Cooper 1981).

Type theory with records is a formal semantics representation framework, using records to express type theory types. It has been used in natural language processing, principally computational semantics and dialogue systems.

Social sciences
Gregory Bateson introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types.

Type theory as a logic
A type theory is a mathematical logic, which is to say it is a collection of rules of inference that result in judgments. Most logics have judgments asserting "The proposition $$\varphi$$ is true", or "The formula $$\varphi$$ is a well-formed formula". A type theory has judgments that define types and assign them to a collection of formal objects, known as terms. A term and its type are often written together as $$\mathrm{term}:\mathsf{type}$$.

Terms
A term in logic is recursively defined as a constant symbol, variable, or a function application, where a term is applied to another term. Constant symbols could include the natural number $$0$$, the Boolean value $$\mathrm{true}$$, and functions such as the successor function $$\mathrm{S}$$ and conditional operator $$\mathrm{if}$$. Thus some terms could be $$0$$, $$(\mathrm{S}\,0)$$, $$(\mathrm{S}\,(\mathrm{S}\,0))$$, and $$(\mathrm{if}\,\mathrm{true}\,0\,(\mathrm{S}\,0))$$.

Judgments
Most type theories have 4 judgments:

 * "$$T$$ is a type"
 * "$$t$$ is a term of type $$T$$"
 * "Type $$T_1$$ is equal to type $$T_2$$"
 * "Terms $$t_1$$ and $$t_2$$ both of type $$T$$ are equal"

Judgments may follow from assumptions. For example, one might say "assuming $$x$$ is a term of type $$\mathsf{bool}$$ and $$y$$ is a term of type $$\mathsf{nat}$$, it follows that $$(\mathrm{if}\,x\,y\,y)$$ is a term of type $$\mathsf{nat}$$". Such judgments are formally written with the turnstile symbol $$\vdash$$.

$$x:\mathsf{bool},y:\mathsf{nat}\vdash(\textrm{if}\,x\,y\,y): \mathsf{nat}$$

If there are no assumptions, there will be nothing to the left of the turnstile.

$$\vdash \mathrm{S}:\mathsf{nat}\to\mathsf{nat}$$

The list of assumptions on the left is the context of the judgment. Capital greek letters, such as $\Gamma$ and $$\Delta$$, are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.

Some textbooks use a triple equal sign $$\equiv$$ to stress that this is judgmental equality and thus an extrinsic notion of equality. The judgments enforce that every term has a type. The type will restrict which rules can be applied to a term.

Rules of Inference
A type theory's inference rules say what judgments can be made, based on the existence of other judgments. Rules are expressed as a Gentzen-style deduction using a horizontal line, with the required input judgments above the line and the resulting judgment below the line. For example, the following inference rule states a substitution rule for judgmental equality.$$ \begin{array}{c} \Gamma\vdash t:T_1 \qquad \Delta\vdash T_1 = T_2 \\ \hline \Gamma,\Delta\vdash t:T_2 \end{array} $$The rules are syntactic and work by rewriting. The metavariables $$\Gamma$$, $$\Delta$$, $$t$$, $$T_1$$, and $$T_2$$ may actually consist of complex terms and types that contain many function applications, not just single symbols.

To generate a particular judgment in type theory, there must be a rule to generate it, as well as rules to generate all of that rule's required inputs, and so on. The applied rules form a proof tree, where the top-most rules need no assumptions. One example of a rule that does not require any inputs is one that states the type of a constant term. For example, to assert that there is a term $$0$$ of type $$\mathsf{nat}$$, one would write the following.$$ \begin{array}{c} \hline \vdash 0 : nat \\ \end{array} $$

Type inhabitation
Generally, the desired conclusion of a proof in type theory is one of type inhabitation. The decision problem of type inhabitation (abbreviated by $$\exists t.\Gamma \vdash t : \tau?$$) is:
 * Given a context $$\Gamma$$ and a type $$\tau$$, decide whether there exists a term $$t$$ that can be assigned the type $$\tau$$ in the type environment $$\Gamma$$.

Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.

A type theory usually has several rules, including ones to:
 * create a judgment (known as a context in this case)
 * add an assumption to the context (context weakening)
 * rearrange the assumptions
 * use an assumption to create a variable
 * define reflexivity, symmetry and transitivity for judgmental equality
 * define substitution for application of lambda terms
 * list all the interactions of equality, such as substitution
 * define a hierarchy of type universes
 * assert the existence of new types

Also, for each "by rule" type, there are 4 different kinds of rules

 * "type formation" rules say how to create the type
 * "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S".
 * "term elimination" rules define the other functions like "first", "second", and "R".
 * "computation" rules specify how computation is performed with the type-specific functions.

For examples of rules, an interested reader may follow Appendix A.2 of the Homotopy Type Theory book, or read Martin-Löf's Intuitionistic Type Theory.

Connections to foundations
The logical framework of a type theory bears a resemblance to intuitionistic, or constructive, logic. Formally, type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic. Additionally, connections can be made to category theory and computer programs.

Intuitionistic logic
When used as a foundation, certain types are interpreted to be propositions (statements that can be proven), and terms inhabiting the type are interpreted to be proofs of that proposition. When some types are interpreted as propositions, there is a set of common types that can be used to connect them to make a Boolean algebra out of types. However, the logic is not classical logic but intuitionistic logic, which is to say it does not have the law of excluded middle nor double negation.

Under this intuitionistic interpretation, there are common types that act as the logical operators:

Because the law of excluded middle does not hold, there is no term of type $$\Pi a.A+ (A\to\bot)$$. Likewise, double negation does not hold, so there is no term of type $$\Pi A.((A\to\bot)\to\bot)\to A$$.

It is possible to include the law of excluded middle and double negation into a type theory, by rule or assumption. However, terms may not compute down to canonical terms and it will interfere with the ability to determine if two terms are judgementally equal to each other.

Constructive mathematics
Per Martin-Löf proposed his intuitionistic type theory as a foundation for constructive mathematics. Constructive mathematics requires when proving "there exists an $$x$$ with property $$P(x)$$", one must construct a particular $$x$$ and a proof that it has property $$P$$. In type theory, existence is accomplished using the dependent product type, and its proof requires a term of that type.

An example of a non-constructive proof is proof by contradiction. The first step is assuming that $$x$$ does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that $$x$$ does not exist". The last step is, by double negation, concluding that $$x$$ exists. Constructive mathematics does not allow the last step of removing the double negation to conclude that $$x$$ exists.

Most of the type theories proposed as foundations are constructive, and this includes most of the ones used by proof assistants. It is possible to add non-constructive features to a type theory, by rule or assumption. These include operators on continuations such as call with current continuation. However, these operators tend to break desirable properties such as canonicity and parametricity.

Curry-Howard correspondence
The Curry–Howard correspondence is the observed similarity between logics and programming languages. The implication in logic, "A $$\to$$ B" resembles a function from type "A" to type "B". For a variety of logics, the rules are similar to expressions in a programming language's types. The similarity goes farther, as applications of the rules resemble programs in the programming languages. Thus, the correspondence is often summarized as "proofs as programs".

The opposition of terms and types can also be viewed as one of implementation and specification. By program synthesis, (the computational counterpart of) type inhabitation can be used to construct (all or parts of) programs from the specification given in the form of type information.

Type inference
Many programs that work with type theory (e.g., interactive theorem provers) also do type inferencing. It lets them select the rules that the user intends, with fewer actions by the user.

Category theory
Main article: Category theory

Although the initial motivation for category theory was far removed from foundationalism, the two fields turned out to have deep connections. As John Lane Bell writes: "In fact categories can themselves be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:
 * cartesian closed categories correspond to the typed λ-calculus (Lambek, 1970);
 * C-monoids (categories with products and exponentials and one non-terminal object) correspond to the untyped λ-calculus (observed independently by Lambek and Dana Scott around 1980);
 * locally cartesian closed categories correspond to Martin-Löf type theories (Seely, 1984).

The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.

Homotopy type theory
Homotopy type theory attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types. Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type. In 2016 cubical type theory was proposed, which is a homotopy type theory with normalization.

Atomic terms
The most basic types are called atoms, and a term whose type is an atom is known as an atomic term. Common atomic terms included in type theories are natural numbers, often notated with the type $$\mathsf{nat}$$, Boolean logic values ($$\mathrm{true}$$/$$\mathrm{false}$$), notated with the type $$\mathsf{bool}$$, and formal variables, whose type may vary. For example, the following may be atomic terms.

 * $$42:\mathsf{nat}$$
 * $$\mathrm{true}:\mathsf{bool}$$
 * $$x:\mathsf{nat}$$
 * $$y:\mathsf{bool}$$

Function terms
In addition to atomic terms, most modern type theories also allow for functions. Function types introduce an arrow symbol, and are defined inductively: If $$\sigma$$ and $$\tau$$ are types, then the notation $$\sigma\to\tau$$ is the type of a function which takes a parameter of type $$\sigma$$ and returns a term of type $$\tau$$. Types of this form are known as simple types.

Some terms may be declared directly as having a simple type, such as the following term, $$\mathrm{add}$$, which takes in two natural numbers in sequence and returns one natural number.

$$\mathrm{add}:\mathsf{nat}\to (\mathsf{nat}\to\mathsf{nat})$$

Strictly speaking, a simple type only allows for one input and one output, so a more faithful reading of the above type is that $$\mathrm{add}$$ is a function which takes in a natural number and returns a function of the form $$\mathsf{nat}\to\mathsf{nat}$$. The parentheses clarify that $$\mathrm{add}$$ does not have the type $$(\mathsf{nat}\to \mathsf{nat})\to\mathsf{nat}$$, which would be a function which takes in a function of natural numbers and returns a natural number. The convention is that the arrow is right associative, so the parentheses may be dropped from $$\mathrm{add}$$'s type.

Lambda terms
New function terms may be constructed using lambda expressions, and are called lambda terms. These terms are also defined inductively: a lambda term has the form $$(\lambda v .t)$$, where $$v$$ is a formal variable and $$t$$ is a term, and its type is notated $$\sigma\to\tau$$, where $$\sigma$$ is the type of $$v$$, and $$\tau$$ is the type of $$t$$. The following lambda term represents a function which doubles an input natural number.

$$(\lambda x.\mathrm{add}\,x\,x): \mathsf{nat}\to\mathsf{nat}$$

The variable is $$  x$$ and (implicit from the lambda term's type) must have type $$    \mathsf{nat} $$. The term $$  \mathrm{add}\,x\,x$$ has type $$    \mathsf{nat} $$, which is seen by applying the function application inference rule twice. Thus, the lambda term has type $$\mathsf{nat}\to\mathsf{nat}$$, which means it is a function taking a natural number as an argument and returning a natural number.

A lambda term is often referred to as an anonymous function because it lacks a name. The concept of anonymous functions appears in many programming languages.

Function application
The power of type theories is in specifying how terms may be combined by way of inference rules. Type theories which have functions also have the inference rule of function application: if $$t$$ is a term of type $$\sigma\to\tau$$, and $$s$$ is a term of type $$\sigma$$, then the application of $$t$$ to $$s$$, often written $$(t\,s)$$, has type $$\tau$$. For example, if one knows the type notations $$0:\textsf{nat}$$, $$1:\textsf{nat}$$, and $$2:\textsf{nat}$$, then the following type notations can be deduced from function application.
 * $$ (\mathrm{add}\,1): \textsf{nat}\to\textsf{nat}$$
 * $$  ((\mathrm{add}\,2)\,0): \textsf{nat}$$
 * $$  ((\mathrm{add}\,1)((\mathrm{add}\,2)\,0)): \textsf{nat}$$

Parentheses indicate the order of operations; however, by convention, function application is left associative, so parentheses can be dropped where appropriate. In the case of the three examples above, all parentheses could be omitted from the first two, and the third may simplified to $$  \mathrm{add}\,1\, (\mathrm{add}\,2\,0): \textsf{nat}$$.

Reductions
Type theories that allow for lambda terms also include inference rules known as $$\beta$$-reduction and $$\eta$$-reduction. They generalize the notion of function application to lambda terms. Symbolically, they are written

 * $$(\lambda v. t)\,s\rightarrow t[v \colon= s]$$ ($$\beta$$-reduction).
 * $$(\lambda v. t\, v)\rightarrow t$$, if $$  v$$ is not a free variable in $$t$$ ($$\eta$$-reduction).

The first reduction describes how to evaluate a lambda term: if a lambda expression $$(\lambda v .t)$$ is applied to a term $$s$$, one replaces every occurrence of $$v$$ in $$t$$ with $$s$$. The second reduction makes explicit the relationship between lambda expressions and function types: if $$(\lambda v. t\, v)$$ is a lambda term, then it must be that $$t$$ is a function term because it is being applied to $$v$$. Therefore, the lambda expression is equivalent to just $$t$$, as both take in one argument and apply $$t$$ to it.

For example, the following term may be $$\beta$$-reduced.

$$(\lambda x.\mathrm{add}\,x\,x)\,2\rightarrow \mathrm{add}\,2\,2$$

In type theories that also establish notions of equality for types and terms, there are corresponding inference rules of $$\beta$$-equality and $$\eta$$-equality.

Empty type
The empty type has no terms. The type is usually written $$\bot$$ or $$\mathbb 0$$. One use for the empty type is proofs of type inhabitation. If for a type $$a$$, it is consistent to derive a function of type $$a\to\bot$$, then $$a$$ is uninhabited, which is to say it has no terms.

Unit type
The unit type has exactly 1 canonical term. The type is written $$\top$$ or $$\mathbb 1$$ and the single canonical term is written $$\ast$$. The unit type is also used in proofs of type inhabitation. If for a type $$a$$, it is consistent to derive a function of type $$\top\to a$$, then $$a$$ is inhabited, which is to say it must have one or more terms.

Boolean type
The Boolean type has exactly 2 canonical terms. The type is usually written $$\textsf{bool}$$ or $$\mathbb B$$ or $$\mathbb 2$$. The canonical terms are usually $$\mathrm{true}$$ and $$\mathrm{false}$$.

Natural numbers
Natural numbers are usually implemented in the style of Peano Arithmetic. There is a canonical term $$0:\mathsf{nat}$$ for zero. Canonical values larger than zero use iterated applications of a successor function $$\mathrm{S}:\mathsf{nat}\to\mathsf{nat}$$.

Dependent typing
Some type theories allow for types of complex terms, such as functions or lists, to depend on the types of its arguments. For example, a type theory could have the dependent type $$\mathsf{list}\,a$$, which should correspond to lists of terms, where each term must have type $$a$$. In this case, $$\mathsf{list}$$ has the type $$U\to U$$, where $$U$$ denotes the universe of all types in the theory.

Some theories also permit types to be dependent on terms instead of types. For example, a theory could have the type $$\mathsf{vector}\,n$$, where $$n$$ is a term of type $$\mathsf{nat}$$ encoding the length of the vector. This allows for greater specificity and type safety: functions with vector length restrictions or length matching requirements, such as the dot product, can encode this requirement as part of the type.

There are foundational issues that can arise from dependent types if a theory is not careful about what dependencies are allowed, such as Girard's Paradox. The logician Henk Barendegt introduced the lambda cube as a framework for studying various restrictions and levels of dependent typing.

Product type
The product type depends on two types, and its terms are commonly written as ordered pairs $$(s,t)$$ or with the symbol $$\times$$. The pair $$(s,t)$$ has the product type $$\sigma\times\tau$$, where $$\sigma$$ is the type of $$s$$ and $$\tau$$ is the type of $$t$$. The product type is usually defined with eliminator functions $$\mathrm{first}:(\Pi\,\sigma\,\tau.\sigma\times\tau\to\sigma)$$ and $$\mathrm{second}:(\Pi\,\sigma\,\tau.\sigma\times\tau\to\tau)$$.

 * $$\mathrm{first}\,(s,t)$$ returns $$s$$, and
 * $$\mathrm{second}\,(s,t)$$ returns $$t$$.

Besides ordered pairs, this type is used for the concepts of logical conjunction and intersection.

Sum type
The sum type depends on two types, and it is commonly written with the symbol $$+$$ or $$\sqcup$$. In programming languages, sum types may be referred to as tagged unions. The type $$\sigma\sqcup\tau$$ is usually defined with constructors $$\mathrm{left}:\sigma\to(\sigma\sqcup\tau)$$ and $$\mathrm{right}:\tau\to(\sigma\sqcup\tau)$$, which are injective, and an eliminator function $$\mathrm{match}:(\Pi\,\rho.(\sigma\to\rho)\to(\tau\to\rho)\to(\sigma\sqcup\tau)\to\rho)$$ such that

 * $$\mathrm{match}\,f\,g\,(\mathrm{left}\,x)$$ returns $$f\,x$$, and
 * $$\mathrm{match}\,f\,g\,(\mathrm{right}\,y)$$ returns $$g\,y$$.

The sum type is used for the concepts of logical disjunction and union.

Dependent products and sums
Two common type dependencies, dependent product and dependent sum types, allow for the theory to encode BHK intuitionistic logic by acting as equivalents to universal and existential quantification; this is formalized by Curry–Howard Correspondence. As they also connect to products and sums in set theory, they are often written with the symbols $$\Pi$$ and $$\Sigma$$, respectively. Dependent product and sum types commonly appear in function types and are frequently incorporated in programming languages.

For example, consider a function $$\mathrm{append}$$, which takes in a $$\mathsf{list}\,a$$ and a term of type $$a$$, and returns the list with the element at the end. The type annotation of such a function would be $$\mathrm{append}:(\Pi\,a.\mathsf{list}\,a\to a\to\mathsf{list}\,a)$$, which can be read as "for any type $$a$$, pass in a $$\mathsf{list}\,a$$ and an $$a$$, and return a $$\mathsf{list}\,a$$".

Sum types are seen in dependent pairs, where the second type depends on the value of the first term. This arises naturally in computer science where functions may return different types of outputs based on the input. For example, the Boolean type is usually defined with an eliminator function $$\mathrm{if}$$, which takes three arguments and behaves as follows. The return type of this function depends on its $$\mathsf{bool}$$ input. If the type theory allows for dependent types, then it is possible to define a function $$\mathrm{TF}\colon\mathsf{bool}\to U\to U\to U$$ such that
 * $$\mathrm{if}\,\mathrm{true}\,x\,y$$ returns $$x$$, and
 * $$\mathrm{if}\,\mathrm{false}\,x\,y$$ returns $$y$$.

 * $$\mathrm{TF}\,\mathrm{true}\,\sigma\,\tau$$ returns $$\sigma$$, and
 * $$\mathrm{TF}\,\mathrm{false}\,\sigma\,\tau$$ returns $$\tau$$.

The type of $$\mathrm{if}$$ may then be written as $$(\Pi\,\sigma\,\tau.\mathsf{bool}\to\sigma\to\tau\to(\Sigma\,x:\textsf{bool}.\mathrm{TF}\,x\,\sigma\,\tau))$$.

Identity type
Following the notion of Curry-Howard Correspondence, the identity type is a type introduced to mirror propositional equivalence, as opposed to the judgmental (syntactic) equivalence that type theory already provides.

An identity type requires two terms of the same type and is written with the symbol $$=$$. For example, if $$x+1$$ and $$1+x$$ are terms, then $$x+1=1+x$$ is a possible type. Canonical terms are created with a reflexivity function, $$\mathrm{refl}$$. For a term $$t$$, the call $$\mathrm{refl}\,t$$ returns the canonical term inhabiting the type $$t=t$$.

The complexities of equality in type theory make it an active research topic; homotopy type theory is a notable area of research that mainly deals with equality in type theory.

Inductive types
Inductive types are a general template for creating a large variety of types. In fact, all the types described above and more can be defined using the rules of inductive types. Two methods of generating inductive types are induction-recursion and induction-induction. A method that only uses lambda terms is Scott encoding.

Some proof assistants, such as Coq and Lean, are based on the calculus for inductive constructions, which is a calculus of constructions with inductive types.

Differences from set theory
The most commonly accepted foundation for mathematics is first-order logic with the language and axioms of Zermelo–Fraenkel set theory with the axiom of choice, abbreviated ZFC. Type theories having sufficient expressibility may also act as a foundation of mathematics. There are a number of differences between these two approaches.

 * Set theory has both rules and axioms, while type theories only have rules. Type theories, in general, do not have axioms and are defined by their rules of inference.
 * Classical set theory and logic have the law of excluded middle. When a type theory encodes the concepts of "and" and "or" as types, it leads to intuitionistic logic, and does not necessarily have the law of excluded middle.
 * In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a predicate function or use a dependently-typed product type, where each element $$x$$ is paired with a proof that the subset's property holds for $$x$$. Where a union would be used, type theory uses the sum type, which contains new canonical terms.
 * Type theory has a built-in notion of computation. Thus, "1+1" and "2" are different terms in type theory, but they compute to the same value. Moreover, functions are defined computationally as lambda terms. In set theory, "1+1=2" means that "1+1" is just another way to refer the value "2". Type theory's computation does require a complicated concept of equality.
 * Set theory encodes numbers as sets. Type theory can encode numbers as functions using Church encoding, or more naturally as inductive types, and the construction closely resembles Peano's axioms.
 * In type theory, proofs are types whereas in set theory, proofs are part of the underlying first-order logic.

Proponents of type theory will also point out its connection to constructive mathematics through the BHK interpretation, its connection to logic by the Curry–Howard isomorphism, and its connections to Category theory.

Properties of type theories
Terms usually belong to a single type. However, there are set theories that define "subtyping".

Computation takes place by repeated application of rules. Many types of theories are strongly normalizing, which means that any order of applying the rules will always end in the same result. However, some are not. In a normalizing type theory, the one-directional computation rules are called "reduction rules", and applying the rules "reduces" the term. If a rule is not one-directional, it is called a "conversion rule".

Some combinations of types are equivalent to other combinations of types. When functions are considered "exponentiation", the combinations of types can be written similarly to algebraic identities. Thus, $${\mathbb 0} + A \cong A$$, $${\mathbb 1} \times A \cong A$$, $${\mathbb 1} + {\mathbb 1} \cong {\mathbb 2}$$, $$A^{B+C} \cong A^B \times A^C$$, $$A^{B\times C} \cong (A^B)^C$$.

Axioms
Most type theories do not have axioms. This is because a type theory is defined by its rules of inference. This is a source of confusion for people familiar with Set Theory, where a theory is defined by both the rules of inference for a logic (such as first-order logic) and axioms about sets.

Sometimes, a type theory will add a few axioms. An axiom is a judgment that is accepted without a derivation using the rules of inference. They are often added to ensure properties that cannot be added cleanly through the rules.

Axioms can cause problems if they introduce terms without a way to compute on those terms. That is, axioms can interfere with the normalizing property of the type theory.

Some commonly encountered axioms are:
 * "Axiom K" ensures "uniqueness of identity proofs". That is, that every term of an identity type is equal to reflexivity.
 * "Univalence Axiom" holds that equivalence of types is equality of types. The research into this property led to cubical type theory, where the property holds without needing an axiom.
 * "Law of Excluded Middle" is often added to satisfy users who want classical logic, instead of intuitionistic logic.

The Axiom of Choice does not need to be added to type theory, because in most type theories it can be derived from the rules of inference. This is because of the constructive nature of type theory, where proving that a value exists requires a method to compute the value. The Axiom of Choice is less powerful in type theory than most set theories, because type theory's functions must be computable and, being syntax-driven, the number of terms in a type must be countable. (See .)

Major

 * Simply typed lambda calculus which is a higher-order logic
 * intuitionistic type theory
 * system F
 * LF is often used to define other type theories
 * calculus of constructions and its derivatives

Minor

 * Automath
 * ST type theory
 * UTT (Luo's Unified Theory of dependent Types)
 * some forms of combinatory logic
 * others defined in the lambda cube (also known as pure type systems)
 * others under the name typed lambda calculus

Active research

 * Homotopy type theory explores equality of types
 * Cubical Type Theory is an implementation of homotopy type theory

Introductory material

 * Type Theory at nLab, which has articles on many topics.
 * Intuitionistic Type Theory article at the Stanford Encyclopedia of Philosophy
 * Lambda Calculi with Types book by Henk Barendregt
 * Calculus of Constructions / Typed Lambda Calculus textbook style paper by Helmut Brandl
 * Intuitionistic Type Theory notes by Per Martin-Löf
 * Programming in Martin-Löf's Type Theory book
 * Homotopy Type Theory book, which proposed homotopy type theory as a mathematical foundation.

Advanced material

 * The TYPES Forum — moderated e-mail forum focusing on type theory in computer science, operating since 1987.
 * The Nuprl Book: "Introduction to Type Theory."
 * Types Project lecture notes of summer schools 2005–2008
 * The 2005 summer school has introductory lectures
 * Oregon Programming Languages Summer School, many lectures and some notes.
 * Summer 2013 lectures including Robert Harper's talks on YouTube
 * Summer 2015 Types, Logic, Semantics, and Verification
 * Andrej Bauer's blog
 * Andrej Bauer's blog

title: Type theory


text:
Melting point

The melting point (or, rarely, liquefaction point) of a substance is the temperature at which it changes state from solid to liquid. At the melting point the solid and liquid phase exist in equilibrium. The melting point of a substance depends on pressure and is usually specified at a standard pressure such as 1 atmosphere or 100 kPa.

When considered as the temperature of the reverse change from liquid to solid, it is referred to as the freezing point or crystallization point. Because of the ability of substances to supercool, the freezing point can easily appear to be below its actual value. When the "characteristic freezing point" of a substance is determined, in fact, the actual methodology is almost always "the principle of observing the disappearance rather than the formation of ice, that is, the melting point."

Examples

For most substances, melting and freezing points are approximately equal. For example, the melting and freezing points of mercury is 234.32 K. However, certain substances possess differing solid-liquid transition temperatures. For example, agar melts at 85 C and solidifies from 31 C; such direction dependence is known as hysteresis. The melting point of ice at 1 atmosphere of pressure is very close to 0 C; this is also known as the ice point. In the presence of nucleating substances, the freezing point of water is not always the same as the melting point. In the absence of nucleators water can exist as a supercooled liquid down to -48.3 C before freezing.

The metal with the highest melting point is tungsten, at 3414 C; this property makes tungsten excellent for use as electrical filaments in incandescent lamps. The often-cited carbon does not melt at ambient pressure but sublimes at about 3700 C; a liquid phase only exists above pressures of 10 MPa and estimated 4,030-4,430 C (see carbon phase diagram). Hafnium carbonitride (HfCN) is a refractory compound with the highest known melting point of any substance to date and the only one confirmed to have a melting point above 4273 K at ambient pressure. Quantum mechanical computer simulations predicted that this alloy (HfN0.38C0.51) would have a melting point of about 4,400 K. This prediction was later confirmed by experiment, though a precise measurement of its exact melting point has yet to be confirmed. At the other end of the scale, helium does not freeze at all at normal pressure even at temperatures arbitrarily close to absolute zero; a pressure of more than twenty times normal atmospheric pressure is necessary.

Melting point measurements
Many laboratory techniques exist for the determination of melting points. A Kofler bench is a metal strip with a temperature gradient (range from room temperature to 300 °C). Any substance can be placed on a section of the strip, revealing its thermal behaviour at the temperature at that point. Differential scanning calorimetry gives information on melting point together with its enthalpy of fusion.

A basic melting point apparatus for the analysis of crystalline solids consists of an oil bath with a transparent window (most basic design: a Thiele tube) and a simple magnifier. Several grains of a solid are placed in a thin glass tube and partially immersed in the oil bath. The oil bath is heated (and stirred) and with the aid of the magnifier (and external light source) melting of the individual crystals at a certain temperature can be observed. A metal block might be used instead of an oil bath. Some modern instruments have automatic optical detection.

The measurement can also be made continuously with an operating process. For instance, oil refineries measure the freeze point of diesel fuel "online", meaning that the sample is taken from the process and measured automatically. This allows for more frequent measurements as the sample does not have to be manually collected and taken to a remote laboratory.

Techniques for refractory materials
For refractory materials (e.g. platinum, tungsten, tantalum, some carbides and nitrides, etc.) the extremely high melting point (typically considered to be above, say, 1,800 °C) may be determined by heating the material in a black body furnace and measuring the black-body temperature with an optical pyrometer. For the highest melting materials, this may require extrapolation by several hundred degrees. The spectral radiance from an incandescent body is known to be a function of its temperature. An optical pyrometer matches the radiance of a body under study to the radiance of a source that has been previously calibrated as a function of temperature. In this way, the measurement of the absolute magnitude of the intensity of radiation is unnecessary. However, known temperatures must be used to determine the calibration of the pyrometer. For temperatures above the calibration range of the source, an extrapolation technique must be employed. This extrapolation is accomplished by using Planck's law of radiation. The constants in this equation are not known with sufficient accuracy, causing errors in the extrapolation to become larger at higher temperatures. However, standard techniques have been developed to perform this extrapolation.

Consider the case of using gold as the source (mp = 1,063 °C). In this technique, the current through the filament of the pyrometer is adjusted until the light intensity of the filament matches that of a black-body at the melting point of gold. This establishes the primary calibration temperature and can be expressed in terms of current through the pyrometer lamp. With the same current setting, the pyrometer is sighted on another black-body at a higher temperature. An absorbing medium of known transmission is inserted between the pyrometer and this black-body. The temperature of the black-body is then adjusted until a match exists between its intensity and that of the pyrometer filament. The true higher temperature of the black-body is then determined from Planck's Law. The absorbing medium is then removed and the current through the filament is adjusted to match the filament intensity to that of the black-body. This establishes a second calibration point for the pyrometer. This step is repeated to carry the calibration to higher temperatures. Now, temperatures and their corresponding pyrometer filament currents are known and a curve of temperature versus current can be drawn. This curve can then be extrapolated to very high temperatures.

In determining melting points of a refractory substance by this method, it is necessary to either have black body conditions or to know the emissivity of the material being measured. The containment of the high melting material in the liquid state may introduce experimental difficulties. Melting temperatures of some refractory metals have thus been measured by observing the radiation from a black body cavity in solid metal specimens that were much longer than they were wide. To form such a cavity, a hole is drilled perpendicular to the long axis at the center of a rod of the material. These rods are then heated by passing a very large current through them, and the radiation emitted from the hole is observed with an optical pyrometer. The point of melting is indicated by the darkening of the hole when the liquid phase appears, destroying the black body conditions. Today, containerless laser heating techniques, combined with fast pyrometers and spectro-pyrometers, are employed to allow for precise control of the time for which the sample is kept at extreme temperatures. Such experiments of sub-second duration address several of the challenges associated with more traditional melting point measurements made at very high temperatures, such as sample vaporization and reaction with the container.

Thermodynamics
For a solid to melt, heat is required to raise its temperature to the melting point. However, further heat needs to be supplied for the melting to take place: this is called the heat of fusion, and is an example of latent heat.

From a thermodynamics point of view, at the melting point the change in Gibbs free energy (ΔG) of the material is zero, but the enthalpy (H) and the entropy (S) of the material are increasing (ΔH, ΔS > 0). Melting phenomenon happens when the Gibbs free energy of the liquid becomes lower than the solid for that material. At various pressures this happens at a specific temperature. It can also be shown that:

 * $$\Delta S = \frac {\Delta H} {T}$$

Here T, ΔS and ΔH are respectively the temperature at the melting point, change of entropy of melting and the change of enthalpy of melting.

The melting point is sensitive to extremely large changes in pressure, but generally this sensitivity is orders of magnitude less than that for the boiling point, because the solid-liquid transition represents only a small change in volume. If, as observed in most cases, a substance is more dense in the solid than in the liquid state, the melting point will increase with increases in pressure. Otherwise the reverse behavior occurs. Notably, this is the case of water, as illustrated graphically to the right, but also of Si, Ge, Ga, Bi. With extremely large changes in pressure, substantial changes to the melting point are observed. For example, the melting point of silicon at ambient pressure (0.1 MPa) is 1415 °C, but at pressures in excess of 10 GPa it decreases to 1000 °C.

Melting points are often used to characterize organic and inorganic compounds and to ascertain their purity. The melting point of a pure substance is always higher and has a smaller range than the melting point of an impure substance or, more generally, of mixtures. The higher the quantity of other components, the lower the melting point and the broader will be the melting point range, often referred to as the "pasty range". The temperature at which melting begins for a mixture is known as the solidus while the temperature where melting is complete is called the liquidus. Eutectics are special types of mixtures that behave like single phases. They melt sharply at a constant temperature to form a liquid of the same composition. Alternatively, on cooling a liquid with the eutectic composition will solidify as uniformly dispersed, small (fine-grained) mixed crystals with the same composition.

In contrast to crystalline solids, glasses do not possess a melting point; on heating they undergo a smooth glass transition into a viscous liquid. Upon further heating, they gradually soften, which can be characterized by certain softening points.

Freezing-point depression
The freezing point of a solvent is depressed when another compound is added, meaning that a solution has a lower freezing point than a pure solvent. This phenomenon is used in technical applications to avoid freezing, for instance by adding salt or ethylene glycol to water.

Carnelley's rule
In organic chemistry, Carnelley's rule, established in 1882 by Thomas Carnelley, states that high molecular symmetry is associated with high melting point. Carnelley based his rule on examination of 15,000 chemical compounds. For example, for three structural isomers with molecular formula C5H12 the melting point increases in the series isopentane −160 °C (113 K) n-pentane −129.8 °C (143 K) and neopentane −16.4 °C (256.8 K). Likewise in xylenes and also dichlorobenzenes the melting point increases in the order meta, ortho and then para. Pyridine has a lower symmetry than benzene hence its lower melting point but the melting point again increases with diazine and triazines. Many cage-like compounds like adamantane and cubane with high symmetry have relatively high melting points.

A high melting point results from a high heat of fusion, a low entropy of fusion, or a combination of both. In highly symmetrical molecules the crystal phase is densely packed with many efficient intermolecular interactions resulting in a higher enthalpy change on melting.

Predicting the melting point of substances (Lindemann's criterion)
An attempt to predict the bulk melting point of crystalline materials was first made in 1910 by Frederick Lindemann. The idea behind the theory was the observation that the average amplitude of thermal vibrations increases with increasing temperature. Melting initiates when the amplitude of vibration becomes large enough for adjacent atoms to partly occupy the same space. The Lindemann criterion states that melting is expected when the vibration root mean square amplitude exceeds a threshold value.

Assuming that all atoms in a crystal vibrate with the same frequency ν, the average thermal energy can be estimated using the equipartition theorem as

E = 4\pi^2 m \nu^2~u^2 = k_{\rm B} T $$ where m is the atomic mass, ν is the frequency, u is the average vibration amplitude, kB is the Boltzmann constant, and T is the absolute temperature. If the threshold value of u2 is c2a2 where c is the Lindemann constant and a is the atomic spacing, then the melting point is estimated as

T_{\rm m} = \cfrac{4\pi^2 m \nu^2 c^2 a^2}{k_{\rm B}}. $$ Several other expressions for the estimated melting temperature can be obtained depending on the estimate of the average thermal energy. Another commonly used expression for the Lindemann criterion is

T_{\rm m} = \cfrac{4\pi^2 m \nu^2 c^2 a^2}{2k_{\rm B}}. $$ From the expression for the Debye frequency for ν,

T_{\rm m} = \cfrac{2\pi m c^2 a^2 \theta_{\rm D}^2 k_{\rm B}}{h^2} $$ where θD is the Debye temperature and h is the Planck constant. Values of c range from 0.15 to 0.3 for most materials.

Databases and automated prediction
In February 2011, Alfa Aesar released over 10,000 melting points of compounds from their catalog as open data and similar data has been mined from patents. The Alfa Aesar and patent data have been summarized in (respectively) random forest and support vector machines.

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

title: Melting point


text:
Cam (mechanism)

A cam is a rotating or sliding piece in a mechanical linkage used especially in transforming rotary motion into linear motion. It is often a part of a rotating wheel (e.g. an eccentric wheel) or shaft (e.g. a cylinder with an irregular shape) that strikes a lever at one or more points on its circular path. The cam can be a simple tooth, as is used to deliver pulses of power to a steam hammer, for example, or an eccentric disc or other shape that produces a smooth reciprocating (back and forth) motion in the follower, which is a lever making contact with the cam. A cam timer is similar, and were widely used for electric machine control (an electromechanical timer in a washing machine being a common example) before the advent of inexpensive electronics, microcontrollers, integrated circuits, programmable logic controllers and digital control.

Camshaft
The cam can be seen as a device that converts rotational motion to reciprocating (or sometimes oscillating) motion. A common example is the camshaft of an automobile, which takes the rotary motion of the engine and converts it into the reciprocating motion necessary to operate the intake and exhaust valves of the cylinders.

Displacement diagram
Cams can be characterized by their displacement diagrams, which reflect the changing position a follower would make as the surface of the cam moves in contact with the follower. In the example shown, the cam rotates about an axis. These diagrams relate angular position, usually in degrees, to the radial displacement experienced at that position. Displacement diagrams are traditionally presented as graphs with non-negative values. A simple displacement diagram illustrates the follower motion at a constant velocity rise followed by a similar return with a dwell in between as depicted in figure 2. The rise is the motion of the follower away from the cam center, dwell is the motion where the follower is at rest, and return is the motion of the follower toward the cam center.

A common type is in the valve actuators in internal combustion engines. Here, the cam profile is commonly symmetric and at rotational speeds generally met with, very high acceleration forces develop. Ideally, a convex curve between the onset and maximum position of lift reduces acceleration, but this requires impractically large shaft diameters relative to lift. Thus, in practice, the points at which lift begins and ends mean that a tangent to the base circle appears on the profile. This is continuous with a tangent to the tip circle. In designing the cam, the lift and the dwell angle $θ$ are given. If the profile is treated as a large base circle and a small tip circle, joined by a common tangent, giving lift $L$, the relationship can be calculated, given the angle $φ$ between one tangent and the axis of symmetry ($φ$ being $π⁄2 − θ⁄2$), while $C$ is the distance between the centres of the circles (required), and $R$ is the radius of the base (given) and $r$ that of the tip circle (required):

 * $C = L⁄1 − sin φ$ and $r = R − L sin φ⁄1 − sin φ$

Disc or plate cam
The most commonly used cam is the cam plate (also known as disc cam or radial cam ) which is cut out of a piece of flat metal or plate. Here, the follower moves in a plane perpendicular to the axis of rotation of the camshaft. Several key terms are relevant in such a construction of plate cams: base circle, prime circle (with radius equal to the sum of the follower radius and the base circle radius), pitch curve which is the radial curve traced out by applying the radial displacements away from the prime circle across all angles, and the lobe separation angle (LSA – the angle between two adjacent intake and exhaust cam lobes).

The base circle is the smallest circle that can be drawn to the cam profile.

A once common, but now outdated, application of this type of cam was automatic machine tool programming cams. Each tool movement or operation was controlled directly by one or more cams. Instructions for producing programming cams and cam generation data for the most common makes of machine, were included in engineering references well into the modern CNC era.

This type of cam is used in many simple electromechanical appliances controllers, such as dishwashers and clothes washing machines, to actuate mechanical switches that control the various parts.

Cylindrical cam
A cylindrical cam or barrel cam is a cam in which the follower rides on the surface of a cylinder. In the most common type, the follower rides in a groove cut into the surface of a cylinder. These cams are principally used to convert rotational motion to linear motion perpendicular to the rotational axis of the cylinder. A cylinder may have several grooves cut into the surface and drive several followers. Cylindrical cams can provide motions that involve more than a single rotation of the cylinder and generally provide positive positioning, removing the need for a spring or other provision to keep the follower in contact with the control surface.

Applications include machine tool drives, such as reciprocating saws, and shift control barrels in sequential transmissions, such as on most modern motorcycles.

A special case of this cam is a constant lead, where the position of the follower is linear with rotation, as in a lead screw. The purpose and detail of implementation influence whether this application is called a cam or a screw thread, but in some cases, the nomenclature may be ambiguous.

Cylindrical cams may also be used to reference an output to two inputs, where one input is the rotation of the cylinder and the other is the position of the follower along the cam. The output is radial to the cylinder. These were once common for special functions in control systems, such as fire control mechanisms for guns on naval vessels and mechanical analog computers.

An example of a cylindrical cam with two inputs is provided by a duplicating lathe, an example of which is the Klotz axe handle lathe, which cuts an axe handle to a form controlled by a pattern acting as a cam for the lathe mechanism.

Face cam
A face cam produces motion by using a follower riding on the face of a disk. The most common type has the follower ride in a slot so that the captive follower produces radial motion with positive positioning without the need for a spring or other mechanism to keep the follower in contact with the control surface. A face cam of this type generally has only one slot for a follower on each face. In some applications, a single element, such as a gear, a barrel cam or other rotating element with a flat face, may do duty as a face cam in addition to other purposes.

Face cams may provide repetitive motion with a groove that forms a closed curve or may provide function generation with a stopped groove. Cams used for function generation may have grooves that require several revolutions to cover the complete function, and in this case, the function generally needs to be invertible so that the groove does not self intersect, and the function output value must differ enough at corresponding rotations that there is sufficient material separating the adjacent groove segments. A common form is the constant lead cam, where the displacement of the follower is linear with rotation, such as the scroll plate in a scroll chuck. Non-invertible functions, which require the groove to self-intersect, can be implemented using special follower designs.

A variant of the face cam provides motion parallel to the axis of cam rotation. A common example is the traditional sash window lock, where the cam is mounted to the top of the lower sash, and the follower is the hook on the upper sash. In this application, the cam is used to provide a mechanical advantage in forcing the window shut, and also provides a self-locking action, like some worm gears, due to friction.

Face cams may also be used to reference a single output to two inputs, typically where one input is the rotation of the cam and the other is the radial position of the follower. The output is parallel to the axis of the cam. These were once common is mechanical analog computation and special functions in control systems.

A face cam that implements three outputs for a single rotational input is the stereo phonograph, where a relatively constant lead groove guides the stylus and tonearm unit, acting as either a rocker-type (tonearm) or linear (linear tracking turntable) follower, and the stylus alone acting as the follower for two orthogonal outputs to representing the audio signals. These motions are in a plane radial to the rotation of the record and at angles of 45 degrees to the plane of the disk (normal to the groove faces). The position of the tonearm was used by some turntables as a control input, such as to turn the unit off or to load the next disk in a stack, but was ignored in simple units.

Heart shaped cam
This type of cam, in the form of a symmetric heart, is used to return a shaft holding the cam to a set position by pressure from a roller. They were used on early models of Post Office Master clocks to synchronise the clock time with Greenwich Mean Time when the activating follower was pressed onto the cam automatically via a signal from an accurate time source.

Snail drop cam
This type of cam was used for example in mechanical timekeeping clocking-in clocks to drive the day advance mechanism at precisely midnight and consisted of a follower being raised over 24 hours by the cam in a spiral path which terminated at a sharp cut off at which the follower would drop down and activate the day advance. Where timing accuracy is required as in clocking-in clocks these were typically ingeniously arranged to have a roller cam follower to raise the drop weight for most of its journey to near its full height, and only for the last portion of its travel for the weight to be taken over and supported by a solid follower with a sharp edge. This ensured that the weight dropped at a precise moment, enabling accurate timing. This was achieved by the use of two snail cams mounted coaxially with the roller initially resting on one cam and the final solid follower on the other but not in contact with its cam profile. Thus the roller cam initially carried the weight, until at the final portion of the run the profile of the non-roller cam rose more than the other causing the solid follower to take the weight.

Linear cam
A linear cam is one in which the cam element moves in a straight line rather than rotates. The cam element is often a plate or block but may be any cross-section. The key feature is that the input is a linear motion rather than rotational. The cam profile may be cut into one or more edges of a plate or block, may be one or more slots or grooves in the face of an element, or may even be a surface profile for a cam with more than one input. The development of a linear cam is similar to, but not identical to, that of a rotating cam.

A common example of a linear cam is a key for a pin tumbler lock. The pins act as followers. This behavior is exemplified when the key is duplicated in a key duplication machine, where the original key acts as a control cam for cutting the new key.

History
Cam mechanisms appeared in China at around 600 BC in the form of a crossbow trigger-mechanism with a cam-shaped swing arm. However, the trigger mechanism did not rotate around its own axis and traditional Chinese technology generally made little use of continuously rotating cams. Nevertheless, later research showed that such cam mechanisms did in fact rotate around its own axis. Likewise, more recent research indicates that cams were used in water-driven trip hammers by the latter half of the Western Han Dynasty (206 BC – 8 AD) as recorded in the Huan Zi Xin Lun. Complex pestles were also mentioned in later records such as the Jin Zhu Gong Zan and the Tian Gong Kai Wu, amongst many other records of water-driven pestles. During the Tang dynasty, the wooden clock within the water-driven astronoical device, the spurs inside a water-driven armillary sphere, the automated alarm within a five-wheeled sand-driven clock, artificial paper figurines within a revolving lantern, all utilized cam mechanisms. The Chinese hodometer which utilized a bell and gong mechanism is also a cam, as described in the Song Shi. In the book Nongshu, the vertical wheel of a water-driven wind box is also a cam. Out of these examples, the water-driven pestle and the water driven wind box both have two cam mechanisms inside. Cams that rotated continuously and functioned as integral machine elements were built into Hellenistic water-driven automata from the 3rd century BC. The cam and camshaft later appeared in mechanisms by Al-Jazari and Shooshtari, who used them in their automata, described in 1206. The cam and camshaft appeared in European mechanisms from the 14th century. Waldo J Kelleigh of Electrical Apparatus Company patented the adjustable cam in the United States in 1956 for its use in mechanical engineering and weaponry.

title: Cam (mechanism)


text:
Talk:Antoine Lavoisier

Wiki Education Foundation-supported course assignment
This article is or was the subject of a Wiki Education Foundation-supported course assignment. Further details are available on the course page. Student editor(s): Stormyruiz. Peer reviewers: JonGreenberger, Analiese Batchelor.

Above undated message substituted from Template:Dashboard.wikiedu.org assignment by PrimeBOT (talk) 17:26, 17 January 2022 (UTC)

Citation and Wording
I feel that the article as a whole requires more citations for certain statements, such as his contributions to proving the law of conservation of mass. Perhaps also there should be a direct citation for the description Lavoisier's system of chemical nomenclature. I'm sure there are other examples of this in the article that I have not mentioned as well.

Also, and this may just be me, but I think the wording used in the chemical revolution section feels somehow biased? It isn't really biased in any way as far as I know, but statements like how Lavoisier's oppositions lacked evidence against him and statements about how precise he was in his measurements feel as though they were made in support of Lavoisier rather than remaining neutral. I also think the phrase "Pioneer of Stoichiometry" shouldn't be used for similar reasons, at least as a title. Maybe "Invention of Stoichiometry" or "Research on Stoichiometry" would feel more neutral?

Gabrielle16 (talk) 17:46, 18 February 2022 (UTC)

Semi-protected edit request on 12 February 2023
Change 55 elements to 33 as per the list here: https://archive.org/details/traitlmentairede01lavo/page/192/mode/2up

The book Creations of Fire (1995) by Cobb also says that Lavoisier only lists 33 elements. TurnerValley (talk) 21:18, 12 February 2023 (UTC)
 * ✅ and thanks for the source! That section is lacking in references. small jars 17:52, 18 February 2023 (UTC)
 * This needs more discussion; SmallJarsWithGreenLabels, you might want to undo pending consensus here. The list on p192 of that linked ref has many more than 33 entries. Are only some of them "elements"? Is there possibly a confusion between the modern definition of "element" and what that word was used to represent at that time? The subsequent sentence in our article likewise lists many more than 33 (and that longer list seems comparable to the linked ref), so it's a dual problem: it's not clear how the ref supports the claim, and it gave us two consecutive sentences that contradicted each other. Cobb's book (e-text ISBN 978-1-4899-2770-5, printed [ISBN 978-0-306-45087-7) is 475 pages; TurnerValley, could you be more speciifc with your citation of it? DMacks (talk) 18:05, 18 February 2023 (UTC)
 * this secondary source (just added) supports a figure of either 33 or 23 depending on the definition. 55 seems like the result of a typo. small jars 18:15, 18 February 2023 (UTC)

Semi-protected edit request on 13 April 2023
please add his spouse to the infobox. His wife was really important in his life. Thank you for helping. Here is the line.

"|spouse     = Marie-Anne Paulze Lavoisier" He King Hung (talk) 10:27, 13 April 2023 (UTC)
 * Not done, it is already there. -- Mvqr (talk) 11:15, 13 April 2023 (UTC)
 * I'm sorry. Blind He King Hung (talk) 14:22, 13 April 2023 (UTC)

Semi-protected edit request on 1 December 2023
The ISBN given for ref # 29 is not a valid ISBN. See https://isbnsearch.org/search?s=0582052940. Please remove the ISBN from the reference. Thank you. 76.14.122.5 (talk) 20:41, 1 December 2023 (UTC)
 * ✅ I've removed the whole source as I cannot find it. I suspect that the actual source is "Citizens: A Chronicle of the French Revolution", but I cannot access the book. Liu1126 (talk) 11:38, 4 December 2023 (UTC)
 * ✅ that edit of yours doesn't appear to have happened? I'm not sure Citizens: A Chronicle of the French Revolution is the same thing. That is listed as a ref in the article, with an author of Simon Schama. The article has several other footnotes for Chronicle of the French Revolution (not Citizens:...) by Jacques Legrand with an ISBN 058205 1 940, one digit off-by-one. I will fix it. But we also do need a page-number, so I will tag it. Yay for checksum! Thanks for raising this concern, 76.14.122.5. DMacks (talk) 13:51, 4 December 2023 (UTC)
 * Well, as soon as the WP database error clears. DMacks (talk) 13:51, 4 December 2023 (UTC)
 * Probably another database error as I didn't check if the edit saved after making it. Been running into them all day for some reason. Liu1126 (talk) 13:54, 4 December 2023 (UTC)
 * Ok, it went through. The database error is known, they're working on it. DMacks (talk) 14:27, 4 December 2023 (UTC)

title: Talk:Antoine Lavoisier


text:
William B. Ogden

William Butler Ogden (June 15, 1805 – August 3, 1877) was an American politician and railroad executive who served as the first Mayor of Chicago. He was referred to as "the Astor of Chicago." He was, at one time, the city's richest citizen.

Early life
Ogden was born on June 15, 1805, in Walton, New York. He was the son of Abraham Ogden (1771–1825) and Abigail (née Weed) Ogden (1788–1850).

When still a teenager, his father died and Ogden took over the family real estate business. He assisted Charles Butler, his brother-in-law, with business matters related to opening a new building for New York University, attending the law school for a brief period himself.

Political career
The first political position Ogden held was as Postmaster of Walton, New York, having been appointed by President Andrew Jackson to the position.

He was a member of the New York State Assembly (Delaware Co.) in 1835.

During his career in New York politics, Ogden was a Jacksonian Democrat. However, Ogden was also an advocate of government funding for infrastructural improvements, aspiring to see the federal government financially back the construction of a railroad from New York to Chicago. He told colleagues that such a railroad would be "the most splendid system of internal communication ever yet devised by man." He had been elected to the New York Senate on a platform supporting state funding for the construction of the New York and Erie Railroad. The bill he backed to accomplish this was passed.

While Ogden's initial concern in Chicago was based in his land interests there, he believed that he could not afford to stay out of the politics of the city, as he believed growing western towns such as Chicago were dependent on government assistance.

Shortly after moving to Chicago in 1836, Ogden joined the committee responsible for drafting the city charter to be submitted to the state legislature.

In 1837, he was elected the first mayor of Chicago, serving a single one-year term. From 1840 through 1841, he served on the Chicago Common Council as an alderman from the 6th Ward. From 1847 through 1848, he served as an alderman from the 9th Ward.

Ogden was a booster of Chicago both during and after his tenures in elected office. At the time he came to Chicago, its buildings were largely wood cabins, it lacked sidewalks and decent bridges, it had no paved roads, and it lacked water supply infrastructure. As a politician he advocated for the city to raise tax revenue for new roads, plank sidewalks, and bridges (which he presented designs of his own for). He also used his own wealth to fund improvements to the city's infrastructure.

Railroad career
Ogden was a leading promoter and investor in the Illinois and Michigan Canal, then switched his loyalty to railroads. Throughout his later life, Ogden was heavily involved in the building of several railroads. "'In 1847, Ogden announced a plan to build a railway out of Chicago, but no capital was forthcoming. Eastern investors were wary of Chicago's reputation for irrational boosterism, and Chicagoans did not want to divert traffic from their profitable canal works. So Ogden and his partner J. Young Scammon solicited subscriptions from the farmers and small businessmen whose land lay adjacent to the proposed rail. Farmer's wives used the money they earned from selling eggs to buy shares of stock on a monthly payment plan. By 1848, Ogden and Scammon had raised $350,000—enough to begin laying track. The Galena and Chicago Union Railroad was profitable from the start and eventually extended out to Wisconsin, bringing grain from the Great Plains into the city. As president of Union Pacific, Ogden extended the reach of Chicago's rail lines to the West coast.'"

In 1853, the Chicago Land Company, of which Ogden was a trustee, purchased land at a bend in the Chicago River and began to cut a channel, formally known as North Branch Canal, but also referred to as Ogden's Canal. The resulting island is now known as Goose Island.

In 1857, Ogden created the Chicago Dock and Canal Company.

Ogden designed the first swing bridge over the Chicago River and donated the land for Rush Medical Center. Ogden was also a founder of the Chicago Board of Trade.

Later Ogden served on the board of the Mississippi and Missouri Railroad and lobbied with many others for congressional approval and funding of the transcontinental railroad. After the 1862 Pacific Railroad Act, Ogden was named as the first president of the Union Pacific Railroad. Ogden was a good choice for the first president, but his railroad experience was most likely not the primary reason he was chosen; Ogden was a clever man who had many political connections. When Ogden came to lead the Union Pacific, the railroad was not fully funded and had not yet laid a single mile of track. The railroad existed largely on paper created by an act of Congress. As part of the 1862 Pacific Railroad Act, Congress named several existing railroad companies to complete portions of the project. Several key areas needed to link the East (Chicago) to the West had none, and hence the Union Pacific was formed by Congress. Ogden was a fierce supporter of the transcontinental railroad at a time of great unrest for the country and was quoted as saying:

"This project must be carried through by even-handed wise consideration and a patriotic course of policy which shall inspire capitalists of the country with confidence. Speculation is as fatal to it as secession is to the Union. Whoever speculates will damn this project."

As history now shows, eventually Ogden and many others got their wish.

Later life

On October 8, 1871, Ogden lost most of his prized possessions in the Great Chicago Fire. He also owned a lumber company in Peshtigo, Wisconsin, which burned the same day.

Personal life
He married Marianna Tuttle Arnot (1825–1904). Marianna was the daughter of Scottish born John Arnot and Harriet (née Tuttle) Arnot. In New York, he named his home in the Highbridge, Bronx (named after the bridge now called Aqueduct Bridge over the Harlem River connecting Manhattan and the Bronx) Villa Boscobel.

Ogden died at his home in the Bronx on Friday, August 3, 1877. The funeral was held August 6, 1877, with several prominent pallbearers including, Gouverneur Morris III, William A. Booth, Parke Godwin, Oswald Ottendorfer, William C. Sheldon, Martin Zborowski, and Andrew H. Green. He was interred at Woodlawn Cemetery, Bronx.

Ogden, who had no children, left behind an estate valued at $10 million in 1877. Some of the money was used to fund a graduate school of science at the Old University of Chicago. Much was left to his niece Eleanor Wheeler, who married Alexander C. McClurg.

Legacy
Namesakes of William B. Ogden include a stretch of U.S. Highway 34, called Ogden Avenue in Chicago and its suburbs, Ogden International School of Chicago, which is located on Walton Street in Chicago, and Ogden Slip, a man-made harbor near the mouth of the Chicago River. Ogden Avenue in The Bronx is also named after him, as is Ogden, Iowa. The Arnot-Odgen Memorial Hospital, founded by his wife Mariana, also bears his namesake. Following his death, William B. Ogden left money to his hometown of Walton, New York, which was used for the construction of a library, completed in 1897, which bears his name, the William B. Ogden Free Library, and is still in use today.

title: William B. Ogden


text:
John Wentworth (Illinois politician)

John Wentworth (March 5, 1815 – October 16, 1888), nicknamed Long John, was the editor of the Chicago Democrat, publisher of an extensive Wentworth family genealogy, a two-term mayor of Chicago, and a six-term member of the United States House of Representatives, both before and after his service as mayor.

After growing up in New Hampshire, he joined the migration west and moved to the developing city of Chicago in 1836, where he made his adult life. Wentworth was affiliated with the Democratic Party until 1855; then he changed to the Republican Party. After retiring from politics, he wrote a three-volume genealogy of the Wentworth family in the United States.

Early life and education
John Wentworth was born in Sandwich, New Hampshire. He was educated at the New Hampton Literary Institute and at the academy of Dudley Leavitt. He graduated from Dartmouth College in 1836.

Migration west and career
Later that year, Wentworth joined a migration west and moved to Chicago, arriving in the city on October 25, 1836. He became managing editor of Chicago's first newspaper, the Chicago Democrat, eventually becoming its owner and publisher.

Wentworth was admitted to the bar in 1841.

He started a law practice and entered politics. He was a business partner of Illinois financier Jacob Bunn, and the two men were two of the incorporators of the Chicago Secure Depository Company.

Marriage and family
In 1844, he married Roxanna Marie Loomis.

In later years, his nephew Moses J. Wentworth handled his business affairs, and would eventually manage his estate as well.

Political career
Wentworth started his political involvement as a Jacksonian democrat, and promoted these views in the Chicago Democrat. After he supported the 1837 mayoral candidacy of William Ogden, including throwing the newspaper behind Ogden's candidacy, he was appointed by Odgen to serve in the post of city printer.

Wentworth, after having become active in Democratic politics, was elected to the U.S. House of Representatives, where he served for a total of six terms, five of them as a Democrat: (March 4, 1843 – March 3, 1851 and March 4, 1853 – March 3, 1855).

He returned to Chicago and affiliated with the Republican Party. Wentworth was first elected mayor in the 1857 Chicago mayoral election; he served two terms, 1857–1858 and 1860–1861 (being elected to his second term in the 1860 Chicago mayoral election). In his second term, he again affiliated with the Democratic Party.

As mayor Wentworth instituted the use of chain gangs of prisoners in the city as laborers.

In July 1857, while serving as mayor of Chicago, Wentworth was charged with assaulting an attorney named Charles Cameron, who was attempting to communicate with his incarcerated client. Cameron testified that Wentworth "seized him by the coat collar and shirt bosom" and forcibly removed him from the prison, alleging that he had resisted officers. Wentworth, after requesting the case be delayed twice, refused to appear in court. The Judge found in favor of Cameron and charged Wentworth amounts of $25 "and costs" and $200. In his effort to clean up the city's morals, he hired spies to determine who was frequenting Chicago's brothels. In 1857, Wentworth led a raid on "the Sands," Chicago's red-light district, which resulted in the burning of the area.

Wentworth served on the Chicago Board of Education.

In 1864, Wentworth ran again for Congress, as a Republican, and was elected for his last term, serving March 4, 1865 – March 3, 1867. While he was in the House, there was a controversial vote to settle a boundary issue between Wisconsin and Illinois, with Wisconsin claiming land as far as the tip of Lake Michigan. Wentworth was promised that if he voted to give the land including Chicago to Wisconsin, he would be appointed to the US Senate. Wentworth declined the offer.

According to city historians in Sandwich, Illinois, Wentworth was one of the key individuals who was responsible for the city getting a railroad stop. The town, which at the time, was called "Newark Station", was given the station, and in turn, the town gave Wentworth the honor of naming the town, which he subsequently named after his hometown, Sandwich, New Hampshire. It is also to note that the boundary line dispute with Wisconsin would have cut through present-day Sandwich, as it straddles the northern border with neighboring LaSalle County, which would have been the State Line had Wentworth not been successful in moving the line north.

After retiring from Congress, from 1868 Wentworth lived at his country estate at 5441 South Harlem Avenue in Chicago. He owned about 5000 acre of land in what is today part of the Chicago neighborhood of Garfield Ridge and suburban Summit.

When an author left a manuscript of a history of Chicago with Wentworth for his suggestions, he reportedly removed what did not refer to him and returned the manuscript to its author with the note, "Here is your expurgated and correct history of Chicago."

Family historian
He researched and wrote The Wentworth Genealogy – English and American - twice, which he published privately. The first two-volume edition, also known as the "private edition", published in 1871, was followed by a second, corrected, edition in 1878, which was published in three volumes, for a total of 2241 pages. The total reported cost for both editions was $40,000. The first of the 1878 volumes chronicles the ancestry of Elder William Wentworth, the first of this family in New England, and his first five generations of New World descendants. The second and third volumes discuss the "Elder's" many descendants and others of the name. John was a fourth great-grandson of William.

Death
Wentworth died at his estate in 1888, aged 73. He was buried in Rosehill Cemetery in Chicago.

At his request, his tombstone was a sixty-foot tall granite obelisk that was imported from New Hampshire on two railroad cars. It was, at the time, the tallest tombstone in the west.

title: John Wentworth (Illinois politician)


text:
Hiram College

Hiram College is a private liberal arts college in Hiram, Ohio. It was founded in 1850 as the Western Reserve Eclectic Institute by Amos Sutton Hayden and other members of the Disciples of Christ Church. The college is nonsectarian and coeducational. It is accredited by the Higher Learning Commission. Among its alumni is James A. Garfield, who also served as a college instructor and principal before he was President of the United States.

History
On June 12, 1849, representatives of the Disciples of Christ voted to establish an academic institution, which would later become Hiram College. On November 7 that year, they chose the village of Hiram as the site for the school because the founders considered this area of the Western Reserve to be "healthful and free of distractions". The following month, on December 20, the founders accepted the suggestion of Isaac Errett and named the school the Western Reserve Eclectic Institute.

The institute's original charter was authorized by the state legislature on March 1, 1850, and the school opened several months later, on November 27. Many of the students came from the surrounding farms and villages of the Western Reserve, but Hiram soon gained a national reputation and students began arriving from other states. On February 20, 1867, the Institute incorporated as a college and changed its name to Hiram College.

During the years before it was renamed Hiram College, 1850–1867, the school had seven principals, the equivalent of today's college presidents. The two that did the most in establishing and defining the nature of the institution were Disciple minister Amos Sutton Hayden, who led the school through its first six years, and James A. Garfield, who had been a student at the institute from 1851 to 1853 and then returned in 1856 as a teacher. As principal, Garfield expanded the institute's curriculum. He left the Institute in 1861 and in 1880 was elected the 20th President of the United States.

In 1870, one of Garfield's best friends and former students, Burke A. Hinsdale, was appointed Hiram's president. Although there were two before him, Hinsdale is considered the college's first permanent president because the others served only briefly. The next president to have a major impact on the college was Ely V. Zollars, who increased enrollment significantly, established a substantial endowment and created a program for the construction of campus buildings. Later presidents who served for at least 10 years were Miner Lee Bates, Kenneth I. Brown, Paul H. Fall, Elmer Jagow, and G. Benjamin Oliver.

In 1931, shortly before Hiram celebrated the 100th anniversary of Garfield's birth, there was a debate in the community about changing the name of the school to Garfield College. There were strong advocates on both sides of the issue. Among the 2,000 guests at the centennial celebration were three generations of Garfield's family, including two of his sons. The idea of changing the college's name was not mentioned at the event and the idea was abandoned.

Principals and presidents

The following is a list of the school's leaders since its founding in 1850.

Principals (Western Reserve Eclectic Institute)

 * 1850–1856 – Amos Sutton Hayden
 * 1857–1861 – James A. Garfield
 * 1861–1864 – Harvey W. Everest (Pro Tem)
 * 1864–1865 – C. W. Heywood (acting)
 * 1865–1866 – Adoniram J. Thomson (managing)
 * 1866–1867 – John M. Atwater

Presidents (Hiram College)

 * 1867–1868 – Silas E. Shepard (acting)
 * 1868–1870 – John M. Atwater (acting)
 * 1870–1882 – Burke A. Hinsdale
 * 1883–1887 – George M. Laughlin
 * 1887–1888 – Colman Bancroft (acting)
 * 1888–1902 – Ely V. Zollars
 * 1902–1903 – James A. Beattie
 * 1903–1905 – Edmund B. Wakefield (acting)
 * 1905–1907 – Carlos C. Rowlison
 * 1907–1930 – Miner Lee Bates
 * 1930–1940 – Kenneth I. Brown
 * 1940–1957 – Paul H. Fall
 * 1957–1965 – Paul F. Sharp
 * 1965–1965 – James N. Primm
 * 1966–1966 – Wendell G. Johnson (acting)
 * 1966–1985 – Elmer Jagow
 * 1986–1989 – Russell Aiuto
 * 1989–1989 – James Norton (interim)
 * 1990–2000 – G. Benjamin Oliver
 * 2000–2002 – Richard J. Scaldini
 * 2003–2014 – Thomas V. Chema
 * 2014–2020 – Lori E. Varlotta
 * 2020–2023 – David P. Haney
 * 2023–2024 – Robert E. Bohrer II

Academics

As of the 2019–20 academic year, Hiram's student body consists of 1,116 undergraduates from 27 states and 11 foreign countries. Of the 81 full–time faculty, 95% hold a Ph.D. or other terminal degree in their field.

Hiram specializes in the education of undergraduate students, though the college does have a small graduate program. Hiram confers the BA, BSN, and MA degrees. The college offers 33 majors and 40 minors for traditional undergraduates, in addition to pre-professional programs for specific fields. Interdisciplinary studies have also been a part of Hiram's curriculum for decades.

Hiram's curriculum requires all students to complete one course in each of nine academic areas: creative methods, interpretive methods, modeling methods, experimental scientific methods, social and cultural analysis, experiencing the world, understanding diversity at home, interdisciplinary, and ethics and social responsibility. Its education plan also includes international study and independent study opportunities, and faculty–guided research projects. Currently, almost all majors require some form of extensive independent project or apprenticeship experience.

Hiram's academic program consists of five schools: Arts, Humantities & Culture; Business & Communication; Education, Civil Leadership & Social Change; Health & Medical Humanities; and Science & Technology.

The college's curriculum is currently marketed under the name Hiram Connect, which involves four steps: First Year Colloquium/Foundations of the Liberal Arts, Declaration of Major, Experiential Learning, and a Capstone Project.

Hiram has five "Centers of Distinction" for interdisciplinary studies: Center for Integrated Entrepreneurship, Center for Scientific Engagement, Center for Literature and Medicine, Garfield Institute for Public Leadership, and Lindsay-Crane Center for Writing and Literature.

Rankings
Hiram was ranked #167 among National Liberal Arts Colleges by U.S. News & World Report in 2012. At the same time, Hiram is currently ranked #67 among Liberal Arts Colleges by Washington Monthly. Also, in 2018, Forbes ranked Hiram at #644 among all colleges and universities in the U.S, and #29 in Ohio. Hiram has regularly been included in The Princeton Review Best Colleges guide, and is one of 40 schools included in Loren Pope's book Colleges That Change Lives.

Hiram is a member of the Annapolis Group, which has been critical of the college rankings process. Hiram is among the signatories of the Presidents Letter.

Athletics
The school's sports teams are called the Terriers. They participate in NCAA Division III and the North Coast Athletic Conference. In men's volleyball and men's wrestling, sports not sponsored by the NCAC, Hiram competes in the Allegheny Mountain Collegiate Conference. Stunt, an all-female cheerleading discipline included in the NCAA Emerging Sports for Women program, competes in the Great Midwest Athletic Conference.

Hiram will join the Presidents' Athletic Conference (PAC) for administrative purposes on July 1, 2024, coinciding with its move to that conference as a men's volleyball associate. It will continue to compete in other NCAC sports through the 2024–25 school year before fully joining the PAC. Hiram had been a full PAC member from 1971 to 1989.

The Hiram College basketball team won the gold medal in the collegiate division of the 1904 Summer Olympics in St. Louis. It was the first time that basketball was part of an Olympics; it was included as a demonstration sport and no foreign teams participated.

The Cleveland Browns held their training camp at Hiram College from 1952 through 1974, making it the longest–tenured training site in the team's history.

The 2014 Hiram vs. Mount St. Joseph women's basketball game was named the Best Moment at the 2015 ESPY Awards. The game featured terminally ill Mount St. Joseph player Lauren Hill in the first of her four college games, which set the all-time attendance record for an NCAA women's game below the Division I level.

Residence life
The college's residential complexes include Booth-Centennial, East Hall, Whitcomb Hall, Miller Hall, Bowler Hall, and the Townhouses.

Student clubs and organizations

Student Senate is the elected student governing body of the college. It serves as a liaison between students and the school's administration, and oversees all student clubs and organizations, collectively called the Associated Student Organizations (ASO). The Kennedy Center Programming Board (KCPB) falls under the auspices of Student Senate, and is responsible for planning educational, social, recreational, and cultural programs.

Hiram has close to 70 registered student clubs and organizations in eight categories: Academic, Greek Social, Musical, Political and Activism, Publications and Communications, Religious, Special Interest and Service, and Sports and Recreation. Fraternities and sororities are not permitted on campus, but there are six Greek social clubs: Delta Chi Lambda, Kappa Sigma Pi, Lambda Lambda Lambda, Phi Beta Gamma, Phi Gamma Epsilon, Phi Kappa Chi, and Greek Social.

Since 1971, Hiram has maintained a chapter of Phi Beta Kappa, the national honor society for the liberal arts. The school has also had a chapter of Omicron Delta Kappa (ODK), a national leadership honor society, since 1962.

Notable alumni and faculty

 * Jean Ankeney – politician, nurse
 * Edna Allyn – first librarian of the Hawaii State Library
 * Miner Searle Bates – historian, and college professor and administrator
 * Laura Bell – author
 * Robert Biscup – orthopaedic surgeon
 * Howard Junior Brown – physician, gay rights advocate
 * Henry Lawrence Burnett – lawyer
 * Allen R. Bushnell – U.S. Representative
 * Russell L. Caldwell – historian and college professor
 * James Anson Campbell – industrialist
 * Sharon Creech – author
 * Martha Derthick – academic
 * Fritz Dreisbach – artist
 * Virginia Fraser – elder rights activist
 * James A. Garfield – 20th President of the United States
 * Lucretia Rudolph Garfield – First Lady of the United States
 * Franklin L. Gilson – jurist and politician
 * Osee M. Hall – U.S. Representative
 * Pamela Helming - New York State Senator
 * Ammon Hennacy – Christian pacifist, anarchist, and member of the Catholic Worker Movement
 * David Brendan Hopes – author, playwright, and poet
 * Jan Hopkins – anchor, CNN
 * Deborah Joseph – computer scientist
 * John Samuel Kenyon – linguist
 * Frank Laporte – professional baseball player
 * Vachel Lindsay – poet
 * Lance Liotta – cancer biologist
 * James Kirby Martin - Historian
 * J. Kevin McMahon – President and CEO, Pittsburgh Cultural Trust
 * Clara Worst Miller – Ashland College professor of Latin and writer
 * Louis Mink – philosopher of history and college professor
 * Horace Ladd Moore – U.S. Representative
 * Wendy Murray – journalist
 * Gilbert Nations - lawyer, professor, and anti-Catholic activist
 * Carol Z. Perez – U.S. Ambassador to Chile
 * Augustus Herman Pettibone – U.S. Representative
 * Benjamin D. Pritchard – Brevetted Brigadier General, United States Army
 * Dean A. Scarborough – chief executive officer of Avery Dennison Corporation
 * Platt Rogers Spencer – originator of Spencarian penmanship
 * Mark W. Spong – roboticist
 * Michael Stanley – singer–songwriter, musician, and radio personality
 * Claude Steele – social psychologist, college professor, and college administrator
 * Howard F. Taylor – sociologist
 * Emma Rood Tuttle — writer, poet
 * Allyn Vine – physicist and oceanographer
 * P. H. Welshimer – minister
 * Tom Wesselmann – artist
 * John J. Whitacre – U.S. Representative
 * Bill White – professional baseball player and broadcaster; President, National League
 * Dempster Woodworth – editor, politician and physician
 * Laurin D. Woodworth – U.S. Representative
 * Harold Bell Wright – author
 * Allyn Abbott Young – economist
 * Elizabeth MacLeod Walls – 15th President of William Jewell College and 14th President of Washington & Jefferson College

title: Hiram College