{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T21:20:39Z","timestamp":1770412839169,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540680840","type":"print"},{"value":"9783540681038","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68103-8_4","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T04:10:07Z","timestamp":1210047007000},"page":"51-68","source":"Crossref","is-referenced-by-count":1,"title":["Finiteness in a Minimalist Foundation"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Ciraulo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giovanni","family":"Sambin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Ciraulo, F., Sambin, G.: Finitary Formal Topologies and Stone\u2019s Representation Theorem. Theoretical Computer Science (to appear)"},{"issue":"1","key":"4_CR2","doi-asserted-by":"publisher","first-page":"28","DOI":"10.2307\/2275174","volume":"57","author":"T. Coquand","year":"1992","unstructured":"Coquand, T.: An Intuitionistic Proof of Tychonoff Theorem. Journal of Symbolic Logic\u00a057(1), 28\u201332 (1992)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR3","volume-title":"Brouwer\u2019s Cambridge Lectures on Intuitionism","year":"1981","unstructured":"van Dalen, D. (ed.): Brouwer\u2019s Cambridge Lectures on Intuitionism. Cambridge University Press, Cambridge (1981)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computation and Logic in the Real World","author":"M.E. Maietty","year":"2007","unstructured":"Maietty, M.E.: Quotients over Minimal Type Theory. In: Cooper, S.B., L\u00f6we, B., Sorbi, A. (eds.) CiE 2007. LNCS, vol.\u00a04497, Springer, Heidelberg (2007)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Maietti, M.E., Sambin, G.: Toward a Minimalist Foundation for Constructive Mathematics. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, Oxford UP. Oxford Logic Guides, vol.\u00a048 (2005)","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"4_CR6","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples (1984)"},{"issue":"4","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.2307\/2275645","volume":"62","author":"S. Negri","year":"1997","unstructured":"Negri, S., Valentini, S.: Tychonoff\u2019s Theorem in the Framework of Formal Topologies. Journal of Symbolic Logic\u00a062(4), 1315\u20131332 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR8","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Peterson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory. Clarendon Press, Oxford (1990)"},{"key":"4_CR9","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1093\/oso\/9780198501275.001.0001","volume-title":"Twenty-Five Years of Constructive Type Theory. Proceedings of a Congress Held in Venice","author":"G. Sambin","year":"1998","unstructured":"Sambin, G., Valentini, S.: Building up a Toolbox for Martin-L\u00f6f Type Theory: Subset Theory. In: Sambin, G., Smith, J. (eds.) Twenty-Five Years of Constructive Type Theory. Proceedings of a Congress Held in Venice, October 1995, pp. 221\u2013240. Oxford University Press, Oxford (1998)"},{"key":"4_CR10","volume-title":"Constructivism in Mathematics: An Introduction","author":"A.S. Troelstra","year":"1988","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction, vol.\u00a01. NorthHolland, Amsterdam (1988)"},{"key":"4_CR11","first-page":"177","volume-title":"Perspectives on negation. Essays in honour of Johan J. de Iongh on his 80th birthday","author":"W. Veldman","year":"1995","unstructured":"Veldman, W.: Some Intuitionistic Variations on the Notion of a Finite Set of Natural Numbers. In: de Swart, H.C.M., Bergman, L.J.M. (eds.) Perspectives on negation. Essays in honour of Johan J. de Iongh on his 80th birthday, pp. 177\u2013202. Tilburg Univ. Press, Tilburg (1995)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Vickers, S.J.: Compactness in Locales and in Formal Topology. In: Banaschewski, B., Coquand, T., Sambin, G. (eds.) Papers presented at the 2nd Workshop on Formal Topology (2WFTop 2002), Venice, Italy, April 04-06, 2002. Annals of Pure and Applied Logic, vol.\u00a0137, pp. 413\u2013438 (2006)","DOI":"10.1016\/j.apal.2005.05.028"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68103-8_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,9]],"date-time":"2021-09-09T21:38:01Z","timestamp":1631223481000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68103-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540680840","9783540681038"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68103-8_4","relation":{},"subject":[]}}