{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:29Z","timestamp":1725484649982},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_40","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:15:38Z","timestamp":1180656938000},"page":"570-584","source":"Crossref","is-referenced-by-count":6,"title":["Markov\u2019s Principle for Propositional Type Theory"],"prefix":"10.1007","author":[{"given":"Alexei","family":"Kopylov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksey","family":"Nogin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"40_CR1","unstructured":"Stuart F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987."},{"key":"40_CR2","unstructured":"Stuart F. Allen. A Non-type-theoretic Definition of Martin-L\u00f6f\u2019s Types. In Proceedings of the Second Symposium on Logic in Computer Science, pages 215\u2013224. IEEE, June 1987."},{"key":"40_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BF01887198","volume":"1","author":"R. C. Backhouse","year":"1989","unstructured":"Roland C. Backhouse, Paul Chisholm, Grant Malcolm, and Erik Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1:19\u201384, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"40_CR4","doi-asserted-by":"crossref","unstructured":"M. J. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"40_CR5","volume-title":"Varieties of Constructive Mathematics","author":"D. Bridges","year":"1988","unstructured":"Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. Cambridge University Press, Cambridge, 1988."},{"key":"40_CR6","volume-title":"Implementing Mathematics with the NuPRL Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cre-mer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panan-gaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the NuPRL Development System. Prentice-Hall, NJ, 1986."},{"key":"40_CR7","unstructured":"Robert L. Constable and Karl Crary. Computational complexity and induction for partial computable functions in type theory. In Preprint, 1998."},{"issue":"1","key":"40_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"Matt Fairtlough and Michael Mendler. Propositional lax logic. Information and Computation, 137(1):1\u201333, 1997.","journal-title":"Information and Computation"},{"key":"40_CR9","unstructured":"Jason J. Hickey. The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, January 2001."},{"key":"40_CR10","unstructured":"Jason J. Hickey, Aleksey Nogin, et al. MetaPRL home page. http:\/\/metaprl.org\/ ."},{"key":"40_CR11","unstructured":"Martin Hofmann. Extensional concepts in intensional Type theory. PhD thesis, University of Edinburgh, Laboratory for Foundations of Computer Science, 1995."},{"issue":"61","key":"40_CR12","first-page":"226","volume":"9\/3","author":"A.A. Markov","year":"1954","unstructured":"A.A. Markov. On the continuity of constructive function. Uspekhi Matematich-eskikh Nauk, 9\/3(61):226\u2013230, 1954. In Russian.","journal-title":"Uspekhi Matematich-eskikh Nauk"},{"key":"40_CR13","first-page":"8","volume":"67","author":"A.A. Markov","year":"1962","unstructured":"A.A. Markov. On constructive mathematics. Trudy Matematicheskogo Instituta imeni V.A. Steklova, 67:8\u201314, 1962. In Russian. English Translation: A.M.S. Translations, series 2, vol.98, pp. 1-9. MR 27#3528.","journal-title":"Trudy Matematicheskogo Instituta imeni V.A. Steklova"},{"key":"40_CR14","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, Amsterdam, 1982. North Holland.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"40_CR15","doi-asserted-by":"crossref","unstructured":"Aleksey Nogin. Quotient types-a modular approach. Technical report, Cornell University, 2001. To appear.","DOI":"10.1007\/3-540-45685-6_18"},{"key":"40_CR16","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1002\/malq.19950410304","volume":"41","author":"E. Palmgren","year":"1995","unstructured":"Erik Palmgren. The Friedman translation for Martin-L\u00f6f\u2019s type theory. Mathematical Logic Quarterly, 41:314\u2013326, 1995.","journal-title":"Mathematical Logic Quarterly"},{"key":"40_CR17","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In Proceedings of the 16th Annual Symposium on Logic in Computer Science, Boston, Massachusetts, June 2001. LICS. To appear.","DOI":"10.1109\/LICS.2001.932499"},{"key":"40_CR18","unstructured":"Simon Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991."},{"key":"40_CR19","volume-title":"Constructivism in Mathematics, An Introduction","author":"A.S. Troelstra","year":"1988","unstructured":"A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction, Vol. I,II. North-Holland, Amsterdam, 1988."},{"key":"40_CR20","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0168-0072(90)90059-B","volume":"50","author":"D. Wijesekera","year":"1990","unstructured":"Duminda Wijesekera. Constructive modal logics I. Annals of Pure and Applied Logic, 50:271\u2013301, 1990.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:21:18Z","timestamp":1556450478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}