Computational Adequacy in an Elementary Topos

Alex Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 Σ 0 1 -sentences).
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication12th International Workshop, CSL’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998. Proceedings
EditorsGeorg Gottlob, Etienne Grandjean, Katrin Seyr
PublisherSpringer-Verlag GmbH
Number of pages20
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'Computational Adequacy in an Elementary Topos'. Together they form a unique fingerprint.

Cite this