From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/997 Path: news.gmane.org!not-for-mail From: Alex Simpson Newsgroups: gmane.science.mathematics.categories Subject: Paper Announcement Date: Wed, 20 Jan 1999 12:28:53 +0000 Message-ID: <22026.199901201228@craro.dcs.ed.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1241017450 28871 80.91.229.2 (29 Apr 2009 15:04:10 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:04:10 +0000 (UTC) To: categories@mta.ca Original-X-From: cat-dist Wed Jan 20 12:24:50 1999 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id JAA15646 for categories-list; Wed, 20 Jan 1999 09:29:38 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: exmh version 2.0.2 2/24/98 Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 34 Xref: news.gmane.org gmane.science.mathematics.categories:997 Archived-At: 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