{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:49:56Z","timestamp":1725493796979},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540140313"},{"type":"electronic","value":"9783540391852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_5","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T16:13:43Z","timestamp":1193415223000},"page":"78-94","source":"Crossref","is-referenced-by-count":4,"title":["Subsets, Quotients and Partial Functions in Martin-L\u00f6f\u2019s Type Theory"],"prefix":"10.1007","author":[{"given":"Jesper","family":"Carlstr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"5_CR1","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)"},{"key":"5_CR2","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press (1990) http:\/\/www.cs.chalmers.se\/Cs\/Research\/Logic\/book\/ ."},{"key":"5_CR3","unstructured":"Cruz-Filipe, L., Spitters, B.: Program extraction from large proof developments. (to appear)"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76 (1988) pp. 95\u2013120","journal-title":"Information and Computation"},{"key":"5_CR5","unstructured":"Capretta, V.: Chap.5: Setoids. In: Abstraction and Computation. PhD thesis, Katholieke Universiteit Nijmegen (2002)"},{"key":"5_CR6","unstructured":"Cruz-Filipe, L.: Formalizing real calculus in Coq. In Carre\u00f1o, V., Mu\u00f1oz, C., Tahar, S., eds.: Theorem Proving in Higher Order Logics. NASA Conference Proceedings (2002)"},{"key":"5_CR7","unstructured":"Sambin, G., Valentini, S.: Building up a toolbox for Martin-L\u00f6f\u2019s type theory: subset theory. In Sambin, G., Smith, J., eds.: Twenty-Five Years of Constructive Type Theory, Oxford University Press (1995) pp. 221\u2013244"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Sambin, G.: Intuitionistic formal spaces \u2014 a first communication. In Skordev, D., ed.: Mathematical Logic and its Applications. (1987) pp. 187\u2013204","DOI":"10.1007\/978-1-4613-0897-3_12"},{"key":"5_CR9","volume-title":"Proceedings of the Dagstuhl Seminar 00231, Topology in Computer Science: Constructivity; Asymmetry and Partiality; Digitalization","author":"G. Sambin","year":"2000","unstructured":"Sambin, G.: Some points in formal topology. In: Proceedings of the Dagstuhl Seminar 00231, Topology in Computer Science: Constructivity; Asymmetry and Partiality; Digitalization, Schloss Dagstuhl, Germany, June, 2000. (to appear)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Kock, A.: The constructive lift monad. Technical Report RS-95-20, BRICS (1995) http:\/\/www.brics.dk\/RS\/95\/20\/ .","DOI":"10.7146\/brics.v2i20.19922"},{"key":"5_CR11","unstructured":"Palmgren, E.: Partial algebras in type theory. Unpublished note. http:\/\/www.math.uu.se\/~palmgren\/ (2002)"},{"key":"5_CR12","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill (1967)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:48:44Z","timestamp":1556920124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}