Computational Adequacy in an Elementary Topos

Alex Simpson

doi:10.1007/10703163_22

Computational Adequacy in an Elementary Topos

Alex Simpson

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

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 language	English
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
Publisher	Springer
Pages	323-342
Number of pages	20
Volume	1584
DOIs	https://doi.org/10.1007/10703163_22
Publication status	Published - 1999

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	1584

Access to Document

10.1007/10703163_22

download 3Accepted author manuscript, 302 KB

http://dx.doi.org/10.1007/10703163_22

Cite this

Simpson, A. (1999). Computational Adequacy in an Elementary Topos. In G. Gottlob, E. Grandjean, & K. Seyr (Eds.), Computer Science Logic: 12th International Workshop, CSL’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998. Proceedings (Vol. 1584, pp. 323-342). (Lecture Notes in Computer Science; Vol. 1584). Springer. https://doi.org/10.1007/10703163_22

@inproceedings{b4ff520be6bc4138b0d99065e6708efa,

title = "Computational Adequacy in an Elementary Topos",

abstract = "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).",

author = "Alex Simpson",

year = "1999",

doi = "10.1007/10703163_22",

language = "English",

volume = "1584",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "323--342",

editor = "Georg Gottlob and Etienne Grandjean and Katrin Seyr",

booktitle = "Computer Science Logic",

}

Simpson, A 1999, Computational Adequacy in an Elementary Topos. in G Gottlob, E Grandjean & K Seyr (eds), Computer Science Logic: 12th International Workshop, CSL’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998. Proceedings. vol. 1584, Lecture Notes in Computer Science, vol. 1584, Springer, pp. 323-342. https://doi.org/10.1007/10703163_22

Computational Adequacy in an Elementary Topos. / Simpson, Alex.
Computer Science Logic: 12th International Workshop, CSL’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998. Proceedings. ed. / Georg Gottlob; Etienne Grandjean; Katrin Seyr. Vol. 1584 Springer, 1999. p. 323-342 (Lecture Notes in Computer Science; Vol. 1584).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Computational Adequacy in an Elementary Topos

AU - Simpson, Alex

PY - 1999

Y1 - 1999

N2 - 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).

AB - 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).

U2 - 10.1007/10703163_22

DO - 10.1007/10703163_22

M3 - Conference contribution

VL - 1584

T3 - Lecture Notes in Computer Science

SP - 323

EP - 342

BT - Computer Science Logic

A2 - Gottlob, Georg

A2 - Grandjean, Etienne

A2 - Seyr, Katrin

PB - Springer

ER -

Computational Adequacy in an Elementary Topos

Abstract / Description of output

Publication series

Access to Document

Fingerprint

Cite this