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).
|Title of host publication||Computer Science Logic|
|Subtitle of host publication||12th International Workshop, CSL’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998. Proceedings|
|Editors||Georg Gottlob, Etienne Grandjean, Katrin Seyr|
|Number of pages||20|
|Publication status||Published - 1999|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin Heidelberg|