The following paper is available by anonymous FTP or over the Web Computational Adequacy in an Elementary Topos We place simple axioms on an elementary topos which suffice for it to provide a denotational model of call-by-value PCF with sum and product types. The model is synthetic in the sense that types are interpreted by their set-theoretic counterparts within the topos. The main result characterises when the model is computationally adequate with respect to the operational semantics of the programming language. We prove that computational adequacy holds if and only if the topos is $1$-consistent (i.e. its internal logic validates only true $\Sigma^0_1$-sentences). This paper is to appear in the forthcoming proceedings of CSL 98. It is available from: http://www.dcs.ed.ac.uk/~als/Research/adequacy.ps.gz ftp://ftp.dcs.ed.ac.uk/pub/als/Research/adequacy.ps.gz Best wishes, Alex Simpson -- Alex Simpson, LFCS, Division of Informatics, University of Edinburgh Email: Alex.Simpson@dcs.ed.ac.uk Tel: +44 (0)131 650 5113 FTP: ftp.dcs.ed.ac.uk/pub/als Fax: +44 (0)131 667 7209 URL: http://www.dcs.ed.ac.uk/home/als