What is a brief but complete explanation of a pure/dependent type system?
Let's have a go. I'll not bother about Girard's paradox, because it distracts from the central ideas. I will need to introduce some presentational machinery about judgments and derivations and such.

Grammar


  Term &nbsp; ::= &nbsp; (Elim) &nbsp; | &nbsp; * &nbsp; | &nbsp; (Var:Term)&rarr;Term &nbsp; | &nbsp; &lambda;Var&map;Term
  
  Elim &nbsp; ::= &nbsp;  Term:Term &nbsp; | &nbsp; Var &nbsp; | &nbsp; Elim Term


The grammar has two mutually defined forms, "terms" which are the general notion of thing (types are things, values are things), including * (the type of types), dependent function types, and lambda-abstractions, but also embedding "eliminations" (i.e. "usages" rather than "constructions"), which are nested applications where the thing ultimately in the function position is either a variable or a term annotated with its type.

Reduction Rules


  (&lambda;y&map;t : (x:S)&rarr;T) s   &rarrw;  t[s:S / y] : T[s:S / x]
  
  (t : T)  &rarrw;  t


The substitution operation t[e / x] replaces every occurrence of the variable x with the elimination e, avoiding name capture. To form an application that can reduce, a lambda term must be annotated by its type to make an elimination. The type annotation gives the lambda-abstraction a kind of "reactivity", allowing application to proceed. Once we reach the point where no more application is happening and the active t : T is being embedded back into the term syntax, we can drop the type annotation.

Let's extend the &rarrw; reduction relation by structural closure: the rules apply anywhere inside terms and eliminations that you can find something matching the left-hand side. Write &rarrw;* for the reflexive-transitive (0-or-more-step) closure of &rarrw;. The resulting reduction system is confluent in this sense:


  If s &rarrw;* p and s &rarrw;* q, then there exists some r such that p &rarrw;* r and q &rarrw;* r.


Contexts


  Context &nbsp; ::= &nbsp; &nbsp; | &nbsp; Context, Var : Term


Contexts are sequences which assign types to variables, growing on the right, which we think of as the "local" end, telling us about the most recently bound variables. An important property of contexts is that it's always possible to choose a variable not already used in the context. We maintain the invariant that the variables ascribed types in the context are distinct.

Judgments


  Judgment &nbsp; ::= &nbsp; Context &vdash; Term has Term &nbsp; | &nbsp; Context &vdash; Elim is Term


That's the grammar of judgments, but how to read them? For a start, &vdash; is the tradional "turnstile" symbol, separating assumptions from conclusions: you can read it informally as "says".


  G &vdash; T has t


means that given context G, type T admits term t;


  G &vdash; e is S


means that given context G, elimination e is given type S.

Judgments have interesting structure: zero or more inputs, one or more subject, zero or more outputs.

INPUTS                   SUBJECT        OUTPUTS
Context |- Term   has    Term
Context |-               Elim      is   Term


That is, we must propose the types of terms in advance and just check them, but we synthesize the types of eliminations.

Typing Rules

I present these in a vaguely Prolog style, writing J -: P1; ...; Pn to indicate that judgment J holds if premises P1 through Pn also hold. A premise will be another judgment, or a claim about reduction.


  Terms
  
  G &vdash; T has t &nbsp; -: &nbsp; T &rarrw; R; &nbsp; G &vdash; R has t
  
  G &vdash; * has *
  
  G &vdash; * has (x:S)&rarr;T &nbsp; -: &nbsp; G &vdash; * has S; &nbsp; G, z:S !- * has T[z / x]
  
  G &vdash; (x:S)&rarr;T has &lambda;y&map;t &nbsp; -: &nbsp; G, z:S &vdash; T[z/x] has t[z/y]
  
  G &vdash; T has (e) &nbsp; -: &nbsp; G &vdash; e is T
  
  Eliminations
  
  G &vdash; e is R &nbsp; -: &nbsp; G &vdash; e is S; &nbsp; S &rarrw; R
  
  G, x:S, G' &vdash; x is S
  
  G &vdash; f s is T[s:S / x] &nbsp; -: &nbsp; G &vdash; f is (x:S)&rarr;T; &nbsp; G &vdash; S has s


And that's it!

Only two rules are not syntax-directed: the rule which says "you can reduce a type before you use it to check a term" and the rule which says "you can reduce a type after you've synthesized it from an elimination". One viable strategy is to reduce types until you've exposed the topmost constructor.

This system is not strongly normalizing (because of Girard's Paradox, which is a liar-style paradox of self-reference), but it can be made strongly normalizing by splitting * into "universe levels" where any values which involve types at lower levels themselves have types at higher levels, preventing self-reference.

This system does, however, have the property of type preservation, in this sense.


  If G &vdash; T has t and G &rarrw;* D and T &rarrw;* R and t &rarrw; r, then D &vdash; R has r.
  
  If G &vdash; e is S and G &rarrw;* D and e &rarrw; f, then there exists R such that S &rarrw;* R and D &vdash; f is R.


Contexts can compute by allowing the terms they contain to compute. That is, if a judgment is valid now, you can compute its inputs as much as you like and its subject one step, and then it will be possible to compute its outputs somehow to make sure the resulting judgment stays valid. The proof is a simple induction on typing derivations, given the confluence of -->*.

Of course, I've presented only the functional core here, but extensions can be quite modular. Here are pairs.


  Term &nbsp; ::= &nbsp; ... &nbsp; | &nbsp; (x:S)*T &nbsp; | &nbsp; s,t
  
  Elim &nbsp; ::= &nbsp; ... &nbsp; | &nbsp; e.head  &nbsp; | &nbsp; e.tail
  
  (s,t : (x:S)*T).head &rarrw; s:S
  
  (s,t : (x:S)*T).tail &rarrw; t:T[s:S / x]
  
  G &vdash; * has (x:S)*T &nbsp; -: &nbsp; G &vdash; * has S; &nbsp; G, z:S &vdash; * has T[z / x]
  
  G &vdash; (x:S)*T has s,t &nbsp; -: &nbsp; G &vdash; S has s; &nbsp; G &vdash; T[s:S / x] has t
  
  G &vdash; e.head is S &nbsp; -: &nbsp; G &vdash; e is (x:S)*T
  
  G &vdash; e.tail is T[e.head / x] &nbsp; -: &nbsp; G &vdash; e is (x:S)*T