{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T11:48:42Z","timestamp":1750074522824},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,2,6]],"date-time":"2008-02-06T00:00:00Z","timestamp":1202256000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Appl Categor Struct"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s10485-008-9124-9","type":"journal-article","created":{"date-parts":[[2008,2,5]],"date-time":"2008-02-05T13:34:36Z","timestamp":1202218476000},"page":"185-197","source":"Crossref","is-referenced-by-count":1,"title":["L\u00e4uchli\u2019s Completeness Theorem from a Topos-Theoretic Perspective"],"prefix":"10.1007","volume":"18","author":[{"given":"Mat\u00edas","family":"Menni","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,2,6]]},"reference":[{"issue":"2","key":"9124_CR1","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/0168-0072(95)00017-8","volume":"77","author":"R.F. Blute","year":"1996","unstructured":"Blute, R.F., Scott, P.J.: Linear L\u00e4uchli semantics. Ann. Pure Appl. Logic 77(2), 101\u2013142 (1996)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"9124_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0022-4049(94)00103-P","volume":"103","author":"A. Carboni","year":"1995","unstructured":"Carboni, A.: Some free constructions in realizability and proof theory. J. Pure Appl. Algebra 103(2), 117\u2013148 (1995)","journal-title":"J. Pure Appl. Algebra"},{"issue":"1","key":"9124_CR3","doi-asserted-by":"crossref","first-page":"200","DOI":"10.2307\/2275186","volume":"57","author":"V. Harnik","year":"1992","unstructured":"Harnik, V., Makkai, M.: Lambek\u2019s categorical proof theory and L\u00e4uchli\u2019s realizability. J. Symbolic Logic 57(1), 200\u2013230 (1992)","journal-title":"J. Symbolic Logic"},{"key":"9124_CR4","doi-asserted-by":"crossref","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol. 43\u201344 of Oxford Logic Guides. The Clarendon Press Oxford University Press, New York (2002)","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"9124_CR5","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North Holland (1952)"},{"key":"9124_CR6","unstructured":"Kock, A.: On a theorem of L\u00e4uchli concerning proof bundles. Unpublished (August 1970)"},{"key":"9124_CR7","doi-asserted-by":"crossref","unstructured":"Kripke, S.A.: Semantical analysis of intuitionistic logic I. In: Formal Systems and Recursive Functions, pp. 92\u2013130. Amsterdam, North Holland (1965)","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"9124_CR8","doi-asserted-by":"crossref","unstructured":"L\u00e4uchli, H.: An abstract notion of realizability for which intuitionistic predicate calculus is complete. In: Kino, A., Myhill, J., Vesley, R.E. (eds.) Intuitionism and Proof Theory (Proc. Conf., Buffalo, N. Y., 1968), pp. 227\u2013234. North Holland (1970)","DOI":"10.1016\/S0049-237X(08)70754-7"},{"key":"9124_CR9","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In: Heller, A. (ed.) Proceedings of the New York Symposium on Applications of Categorical Logic, pp. 1\u201314. Providence (1970)","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"9124_CR10","unstructured":"Lawvere, F.W.: Adjoints in and among bicategories. In: Logic and Algebra, Lecture Notes in Pure and Applied Algebra, vol. 180, pp. 181\u2013189. Proceedings of the 1994 Siena Conference in Memory of Roberto Magari. Marcel Dekker, Inc. (1996)"},{"key":"9124_CR11","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Adjointness in foundations. Reprints in Theory and Applications of Categories, pp. 1\u201316 (2006), Originally published: Dialectica\u00a023 (1969)","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"issue":"1\u20133","key":"9124_CR12","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0168-0072(96)00002-4","volume":"81","author":"J. Lipton","year":"1996","unstructured":"Lipton, J., O\u2019Donnell, M.J.: Some intuitions behind realizability semantics for constructive logic: Tableaux and L\u00e4uchli countermodels.. Ann. Pure Appl. Logic 81(1\u20133), 187\u2013239 (1996)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9124_CR13","unstructured":"Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic: a First Introduction to Topos Theory. Universitext. Springer Verlag (1992)"},{"key":"9124_CR14","doi-asserted-by":"crossref","unstructured":"Makkai, M.: The fibrational formulation of intuitionistic predicate logic 1: completeness according to G\u00f6del, Kripke and L\u00e4uchli. Parts 1 and 2. Notre Dame J. Formal Logic 34(3 and 4 resp.), 334\u2013377, 471\u2013498 (1993)","DOI":"10.1305\/ndjfl\/1093633902"},{"key":"9124_CR15","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1016\/j.jpaa.2006.10.009","volume":"210","author":"M. Menni","year":"2007","unstructured":"Menni, M.: Cocomplete toposes whose exact completions are toposes. J. Pure Appl. Algebra 210, 511\u2013520 (2007)","journal-title":"J. Pure Appl. Algebra"},{"key":"9124_CR16","doi-asserted-by":"crossref","unstructured":"Paris, A.: L\u00e4uchli realizability and gauge theories. Abstract in the 2000 annual meeting of the Association for Symbolic Logic, June 2000. Bull. Symbolic Logic 6(3)","DOI":"10.2307\/421070"},{"key":"9124_CR17","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 5. Algebraic and Logical Structures, chapter\u00a02. Oxford University Press (2000)","DOI":"10.1093\/oso\/9780198537816.003.0005"}],"container-title":["Applied Categorical Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10485-008-9124-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10485-008-9124-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10485-008-9124-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,21]],"date-time":"2024-02-21T23:04:26Z","timestamp":1708556666000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10485-008-9124-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,2,6]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["9124"],"URL":"https:\/\/doi.org\/10.1007\/s10485-008-9124-9","relation":{},"ISSN":["0927-2852","1572-9095"],"issn-type":[{"value":"0927-2852","type":"print"},{"value":"1572-9095","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,2,6]]}}}