Paper Announcement

[Alex Simpson <als@dcs.ed.ac.uk>]

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