September 2003

Added toProofs a remark about negative hyp number references.

Added some paraphrases for the standard propositional ops inPropositions .

ReworkedPropositions as Types to incorporate a brief treatment of computational content and dropped its references to the merely planned pages about it; also adjustedPropositions as Types - standard defs ,Propositions , andPropositional Proof Witness Extraction similarly.

August 2003

Began reformatting documents to make the more suitable as printable pages.

January 2003

Added a documentSubtyping Relation about advance adoption of the subtype relation primitive.

Added a new extensional fixedpoint theoremThm* A:Type. Sexpr(A) =ext (Sexpr(A)Sexpr(A))+A

toRecursive Types (a note from Kreitz prompted this).

November 2002

Added toOperator Definition indication that function applications,"<fun>(<arg>)" can be used on the lhs of an opdef instead of lambdas,"[var].<*>" , on the rhs.

Added a new theorem about polymorphic functionsThm* f:(D:Type.DT),A:Type,a:A,B:Type,b:B.f(a) =f(b)T

toPolymorphism ( Barzilay suggested adding this).

December 2001

Corrected an erroneousinl( tob)inr( inb)Computation .

Indicatedrec( as an example failure of type formation inX.(X))Recursive Types .

October 2001

Added a reference toThm* whatever1 = whatever2 ( inx:Void. Whatever(x))Intersection Types .

Added a mention ofDec( toP)Propositions as Types .

AddedThm* Dec( toP) (b:.Pb)primitive foropsemblemthmsProps as Types .

September 2001

Corrected some small errors inPolymorphism , and added more thms as examples.

Added a thm citation toPairs .

Added some thm citations toLists .

Added a thm citation and some material about outl,inl,isl toDisjoint Union .

Added a thm citation toIntersection Types

Added a thm citation toQuotient Types .

Added some thm citations about extensionalty toFunction Types .

AddedTyping Y andTyping Y Continued about how to type theY combinator if we extend the Function Extensionality rule.

Addedprimitive (partial index to documents by emblamatic theorem).opsemblemthms

August 2001

Moved the reference toVoid inNuprl Basics .

Added much more material toVoid .

AddedPolymorphism .

Added references toTop toUnit ,Intersection Types ,Quotient Types .

AddedSubtype Relation .

Added reference toSubtype Relation toType Expressions .

Added"Squiggle" and linked to it fromTypes .

May 2001

InBoolean added a demonstration of where implicit-to- Prop coercions occurred inThm* .p,q:. (pq)p&q

InProp Levels and Predicativity changed "predicative logic" to "predicative semantics".

I changed the suggested reading order ofSubstitution andOp Def Restrictions inNuprl Basics .

InOp Def Restrictions , I eliminated a true but distracting parenthetical comment about the left hand side not being too general. I also glossed"second-order variable" as a link.

Added a caveat toFunctions to not identify computational evaluation with an expressions standing for a value.

Added a missing condition toOp Def Restrictions , namely "Distinct subterm positions of the left-hand side must be filled by distinct variables."

CorrectedUniverses to useas domain of V( instead ofi).

April 2001

AddedPropositional Proof Witness Extraction .

About: