Types for Proofs and Programs International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers Coquand Thierry Heftet / 2000 / Engelsk