Located operators

Autor: Spitters, B.A.W.

Publikováno v: Mathematical Logic Quarterly, 48, 1, pp. 107-122
Mathematical Logic Quarterly, 48(S1), 107-122. Wiley-VCH Verlag
Mathematical Logic Quarterly, 48, 107-122

We study operators with located graph in Bishop-style constructive mathematics. It is shown that a bounded operator has an adjoint if and only if its graph is located. Locatedness of the graph is a necessary and sufficient condition for an unbounded

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3ea391ff73591e33f26f6faa0d5d485f
https://doi.org/10.1002/1521-3870(200210)48:1+<107::AID-MALQ107>3.0.CO

Computer Certified Efficient Exact Reals in Coq

Autor: Krebbers, R.J., Spitters, B.A.W., Davenport, J., Farmer, W., Urban, J., Rabe, F.

Publikováno v: Davenport, J.; Farmer, W.; Urban, J. (ed.), Intelligent Computer Mathematics :18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pp. 90-106
Lecture Notes in Artificial Intelligence ; 6824, 90-106. Berlin : Springer
STARTPAGE=90;ENDPAGE=106;TITLE=Lecture Notes in Artificial Intelligence ; 6824
Lecture Notes in Computer Science ISBN: 9783642226724

Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer ha

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cdb70d9ff94d32c6cf7ae5249c0b12de
https://hdl.handle.net/2066/91656

Developing the algebraic hierarchy with type classes in Coq

Autor: Spitters, B.A.W., Weegen, E.E. van der, Kaufmann, M.

Publikováno v: Lecture notes in computer science ; 6172, 490-493. Berlin : Springer
STARTPAGE=490;ENDPAGE=493;TITLE=Lecture notes in computer science ; 6172
Kaufmann, M. (ed.), Interactive Theorem Proving : first International Conference on Interactive Theorem Proving, ITP 2010; Edinburgh; 11 July 2010 through 14 July 2010; proceedings, pp. 490-493

Contains fulltext : 83812.pdf (Publisher’s version ) (Closed access)

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::33895ef415ab27561d9bfe225c599210
https://hdl.handle.net/2066/83812

Bohrification of operator algebras and quantum logic

Autor: Heunen, C., Landsman, N.P., Spitters, B.A.W.

Following Birkhoff and von Neumann, quantum logic has traditionally been based on the lattice of closed linear subspaces of some Hilbert space, or, more generally, on the lattice of projections in a von Neumann algebra A. Unfortunately, the logical i

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=narcis______::c9bf1d9cf237127dbcd6f7608487fc4f
https://research.tue.nl/nl/publications/eb8377cb-6fd9-45e8-a4e5-e17cdbee9592

Computable sets : located and overt locales

Autor: Coquand, T., Spitters, B.A.W.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=narcis______::59b994298b7e1534fcf1f185f394eab8
https://research.tue.nl/nl/publications/dc8c346d-c306-44af-8985-d6a8e95a00ae