[TYPES] Co-algebraic semantics of typed lambda-calculus

[Jacques Carette]

I have been able to find some references to the co-algebraic structure 
(i.e. final semantics) of the untyped lambda-calculus, (work of Honsell 
and Lenisa, available at
http://citeseer.ist.psu.edu/95166.html
and
http://portal.acm.org/citation.cfm?id=645892.671579&coll=&dl=ACM&CFID=15151515&CFTOKEN=6184618 
), but my search for a typed analogue has not turned up anything.  I 
rather suspect that this has already been done - could someone here 
provide me with some references?

Thanks,
Jacques