Errata for Advanced Topics in Types and Programming Languages,
	   Chapter 2, Dependent Types. David Aspinall and Martin Hofmann.

If you find a mistake not listed here, please drop a line
to da@inf.ed.ac.uk, thanks!

Credits:   Christopher Richards; Ethan Aubin; Luke Simon.

---------------------------------------------------------------------

p. 48:  "Pi x:A.B(a)" should be "Pi x:A.B(x)"

p. 56:  "premises to conclusion" should be "conclusion to premises"

p. 60:  Exercises 2.4.5 and 2.5.6 do *not* have solutions
        in the back of the book even though they are not labelled
        to say that, and it is claimed at the end of the previous
        proof that they are "exercises with solutions"!

p. 60:  In exercise 2.4.6, the last statement has a mistake in 
        subscripting, it should be "Gamma |-> t_1 t_2 = s_1 s_2"
        (not "Gamma |-> t_{1t2} = s_{1s2}")

p. 61:  In the final paragraph of the proof of 2.4.10: 
        "Gamma |- t_2:S_2" should be "Gamma |- t_2:T_1"

p. 62:  In figure 2-5, the new syntax for the typed pair uses the
        wrong font for the right parenthesis.

p. 62:  S:T->* should be S::T->*  (it is a kinding not a typing)

p. 65: 	Replace "Nat" by "Prf nat" in the definition of "add" and the 
        later comment about existential quantification. 

p. 65:  In the definition of exists and the Exercise 2.6.1, the
        quantification should be over A rather than Prop, to match
        the type of f.  Replace "Pi x:Prop" with "Pi x:A" and
	"Pi a:Prop" with "Pi a:A". 

p. 66: 	In the proof of 2.6.5, there is a missing space between
       	"mapping" and "eq a t_1 t_2".

p. 67:  In figure 2-8, in the definition of QA-ALL-E "S_1"
        should be "S" and "T_1" should be "T".

p. 68:  In the definition of vecInd, "Prf (p y)" should be
        "Prf (p x y)".

p. 70:  "Pr" should be "Prf" (in display after "together with an
         equality rule..").  

p. 70:  In the definition of the mapping i, "zero:prop" should be
        "zero:Prf prop".

p. 72:  In figure 2-9, Gamma |- S:* should be Gamma |- S:s_i (so
        that the abstractions in the table on p.73 can be formed). 

p. 73:  "Lambda-Cube" in subsection heading should be "Lambda Cube"

p. 74: 	Last paragraph: typo "Undecidablef" should be "Undecidable"

p. 76: 	The last line of "append-body" lacks a right-parenthesis.
       	The corresponding proof obligation (beginning
       	"\Gamma, r:int, ...") also lacks a right-parenthesis.

p. 81: 	The "tighter" typing is for "andalso", not "orelse".

p. 82:  In main-body there is an argument missing to leq:
        replace "(plus[x,y](xx,yy))" with "(plus[x,y](xx,yy),10)".

p. 86:  "\lambda-Cube" sould be "Lambda Cube" for consistency.

p. 495: Solution 2.1.4: in the type of evalLam, ft2 should be ft1'

p. 496: Solution 2.8.1: 
        Third clause for satisfaction between environments and
        contexts should read "eta |= Gamma,P if eta |= Gamma and eta |= P"
        "z in Z" should be "z in [[I]]_eta".
	Delete extra punctuation "." in the final line before
	the implication ==>.


---------------------------------------------------------------------

$Id: errata.txt,v 1.5 2005/06/10 14:30:10 da Exp $