Document Open Access Logo

Realizability Toposes from Specifications

Author Jonas Frey

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.196.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Jonas Frey

Cite As Get BibTex

Jonas Frey. Realizability Toposes from Specifications. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 196-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.196

Abstract

We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using ad- equate interpretations of the central concepts of pole and proof-like term. This method does in particular allow to associate realizability models to computable functions.
Following recent work of Streicher and others we show how these models give rise to triposes and toposes.

Subject Classification

Keywords
  • Krivine machine
  • classical realizability
  • realizability topos
  • bisimulation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. H.P. Barendregt. The lambda calculus, Its syntax and semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, revised edition, 1984. Google Scholar
  2. W. Ferrer, J. Frey, M. Guillermo, O. Malherbe, and A. Miquel. Ordered combinatory algebras and realizability. arXiv preprint arXiv:1410.5034, 2014. Google Scholar
  3. H. Friedman. Classically and intuitionistically provably recursive functions. In Higher set theory (Proc. Conf., Math. Forschungsinst., Oberwolfach, 1977), volume 669 of Lecture Notes in Math., pages 21-27. Springer, Berlin, 1978. Google Scholar
  4. A. Grothendieck, M. Artin, and J.L. Verdier. Théorie des topos et cohomologie étale des schémas. Lecture Notes in Mathematics, 269, 1972. Google Scholar
  5. J. Roger Hindley and Jonathan P. Seldin. Lambda-calculus and combinators, an introduction. Cambridge University Press, Cambridge, 2008. Google Scholar
  6. J.M.E. Hyland. The effective topos. In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pages 165-216. North-Holland, Amsterdam, 1982. Google Scholar
  7. J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc., 88(2):205-231, 1980. Google Scholar
  8. B. Jacobs. Categorical logic and type theory. Elsevier Science Ltd, 2001. Google Scholar
  9. J.L. Krivine. Lambda-calcul, évaluation paresseuse et mise en mémoire. RAIRO Inform. Théor. Appl., 25(1):67-84, 1991. Google Scholar
  10. J.L. Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009. Google Scholar
  11. J.L. Krivine. Realizability algebras: a program to well order ℝ. Log. Methods Comput. Sci., 7(3):3:02, 47, 2011. Google Scholar
  12. J.L. Krivine. Realizability algebras II: New models of ZF+DC. Log. Methods Comput. Sci., 8(1):1:10, 28, 2012. Google Scholar
  13. R. Milner. Operational and algebraic semantics of concurrent processes. In Handbook of theoretical computer science, Vol. B, pages 1201-1242. Elsevier, Amsterdam, 1990. Google Scholar
  14. A. Miquel. Classical modal realizability and side effects. preprint, 2009. Google Scholar
  15. A. Miquel. Existential witness extraction in classical realizability and via a negative translation. Log. Methods Comput. Sci., 7(2):2:2, 47, 2011. Google Scholar
  16. A. Miquel. Forcing as a program transformation. In 26th Annual IEEE Symposium on Logic in Computer Science - LICS 2011, pages 197-206. IEEE Computer Soc., Los Alamitos, CA, 2011. Google Scholar
  17. W.P. Stekelenburg. Realizability Categories. PhD thesis, Utrecht University, 2013. Google Scholar
  18. T. Streicher. Krivine’s classical realisability from a categorical perspective. Mathematical Structures in Computer Science, 23(06):1234-1256, 2013. Google Scholar
  19. A.S. Troelstra and H. Schwichtenberg. Basic proof theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1996. Google Scholar
  20. J. van Oosten. Classical Realizability. Invited talk at "Cambridge Category Theory Seminar", slides at URL: http://www.staff.science.uu.nl/~ooste110/talks/cambr060312.pdf.
  21. J. van Oosten. Realizability: An Introduction to its Categorical Side. Elsevier Science Ltd, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact