{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T18:34:06Z","timestamp":1723487646567},"reference-count":14,"publisher":"Wiley","issue":"3","license":[{"start":{"date-parts":[[2006,11,13]],"date-time":"2006-11-13T00:00:00Z","timestamp":1163376000000},"content-version":"vor","delay-in-days":4334,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[1995,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin\u2010L\u00f6f's type theory, inlcuding universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule.<\/jats:p>","DOI":"10.1002\/malq.19950410304","type":"journal-article","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T17:47:03Z","timestamp":1180201623000},"page":"314-326","source":"Crossref","is-referenced-by-count":3,"title":["The Friedman\u2010Translation for Martin\u2010L\u00f6f's Type Theory"],"prefix":"10.1002","volume":"41","author":[{"given":"Erik","family":"Palmgren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2006,11,13]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"e_1_2_1_3_2","unstructured":"Coquand T. andH.Herbelin An application of A\u2010translation to the existence of families of looping combinators in inconsistent type systems. Manuscript1991."},{"key":"e_1_2_1_4_2","first-page":"21","volume-title":"Classically and intuitionistically provably recursive functions. In: Higher Set Theory","author":"Friedman H.","year":"1978"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.2307\/2274322"},{"key":"e_1_2_1_6_2","unstructured":"Martin\u2010L\u00f6f P. Intuitionistic Type Theory. Bibliopolis Padova1984."},{"key":"e_1_2_1_7_2","unstructured":"Murthy C. Extracting constructive content from classical proofs. Ph.D. Thesis Cornell University1990."},{"key":"e_1_2_1_8_2","volume-title":"Programming in Martin\u2010L\u00f6f's type theory","author":"Nordstr\u00f6m B.","year":"1990"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01269951"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90044-3"},{"key":"e_1_2_1_11_2","unstructured":"Salvesen A. On information discharging and retrieval in Martin\u2010L\u00f6f's type theory. Doctoral dissertation University of Oslo1989."},{"key":"e_1_2_1_12_2","unstructured":"Schwichtenberg H. A normal form for natural deductions in a type theory with realizing terms. In:Atti del Congresso Logica e Filosofia della Scienza oggi. San Gimignano 7\u201311 dicembre 1983 Vol I (Logica) CLUEB Bologna1986 pp.95\u2013138."},{"key":"e_1_2_1_13_2","first-page":"331","volume-title":"Proceedings of the Conference on Logic and its Applications, Bulgaria 1986","author":"Smith J. M.","year":"1987"},{"key":"e_1_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.2307\/2274575"},{"key":"e_1_2_1_15_2","volume-title":"Constructivism in Mathematics","author":"Troelstra A. S.","year":"1988"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.19950410304","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.19950410304","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,26]],"date-time":"2023-10-26T14:45:50Z","timestamp":1698331550000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.19950410304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["10.1002\/malq.19950410304"],"URL":"https:\/\/doi.org\/10.1002\/malq.19950410304","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}