{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:22Z","timestamp":1725663682530},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569923"},{"type":"electronic","value":"9783540478904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56992-8_20","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:00:09Z","timestamp":1330257609000},"page":"340-351","source":"Crossref","is-referenced-by-count":4,"title":["Universes in the theories of types and names"],"prefix":"10.1007","author":[{"given":"Markus","family":"Marzetta","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"20_CR1","volume-title":"Foundations of Constructive Mathematics","author":"M. J. Beeson","year":"1984","unstructured":"M. J. Beeson. Foundations of Constructive Mathematics. Springer, Berlin, 1984."},{"key":"20_CR2","series-title":"volume 450 of LNM","volume-title":"Algebra and Logic","author":"S. Feferman","year":"1975","unstructured":"S. Feferman. A language and axioms for explicit mathematics. In Algebra and Logic, volume 450 of LNM, Berlin, 1975. Springer."},{"key":"20_CR3","volume-title":"Logic Colloquium '78","author":"S. Feferman","year":"1978","unstructured":"S. Feferman. Constructive theories of functions and classes. In Boffa, editor, Logic Colloquium '78, Amsterdam, 1978. North-Holland."},{"key":"20_CR4","volume-title":"Patras Logic Symposion","author":"S. Feferman","year":"1982","unstructured":"S. Feferman. Iterated inductive fixed-point theories: application to Hancock's conjecture. In Metakides, editor, Patras Logic Symposion, Amsterdam, 1982. North-Holland."},{"key":"20_CR5","unstructured":"S. Feferman. Logics for termination and correctness of functional programs, II. Logics of Strength PRA. Lecture notes for the Summer School and Conference on Proof Theory in Leeds, 30 July\u20132 August 1990."},{"key":"20_CR6","volume-title":"Logic from Computer Science","author":"S. Feferman","year":"1992","unstructured":"S. Feferman. Logics for termination and correctness of functional programs. In Moschovakis, editor, Logic from Computer Science, New York, 1992. Springer."},{"key":"20_CR7","unstructured":"H. Friedman. Systems of second order arithmetic with restricted induction (abstracts). Journal for Symbolic Logic, 41, 1976."},{"key":"20_CR8","volume-title":"Patras Logic Symposion","author":"H. M. Friedman","year":"1982","unstructured":"H. M. Friedman, K. McAloon, and S. G. Simpson. A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis. In Metakides, editor, Patras Logic Symposion, Amsterdam, 1982. North-Holland."},{"issue":"1","key":"20_CR9","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0304-3975(90)90108-T","volume":"89","author":"Robert Harper","year":"1991","unstructured":"R. Harper and R. Pollack. Type checking with universes. Theoretical Computer Science, 89, 1991.","journal-title":"Theoretical Computer Science"},{"issue":"03","key":"20_CR10","doi-asserted-by":"crossref","first-page":"867","DOI":"10.2307\/2274140","volume":"49","author":"Gerhard J\u00e4ger","year":"1984","unstructured":"G. J\u00e4ger. The strength of admissibility without foundation. Journal for Symbolic Logic, 49(3), 1984.","journal-title":"The Journal of Symbolic Logic"},{"key":"20_CR11","unstructured":"G. J\u00e4ger. Induction in the elementary theory of types and names. In B\u00f6rger, editor, Proceedings CSL '87. Springer, 1987. LNCS 329."},{"key":"20_CR12","unstructured":"R. Kahle. Theorien von Operationen und Klassen zur Beschreibung von ML-Programmen. Master's thesis, Mathematisches Institut, Universit\u00e4t M\u00fcnchen, 1993."},{"key":"20_CR13","volume-title":"Logic Colloquium '73","author":"P. Martin-L\u00f6f","year":"1975","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types: predicative part. In Rose and Shepherdson, editors, Logic Colloquium '73, Amsterdam, 1975. North-Holland."},{"key":"20_CR14","unstructured":"P. Martin-L\u00f6f. Intutionistic Type Theory. Bibliopolis, 1984."},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell and R. Harper. The essence of ML. In Proc. of the 15th Annual ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. ACM, 1988.","DOI":"10.1145\/73560.73563"},{"key":"20_CR16","volume-title":"Programming in Martin-L\u00f6f's Type Theory: An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f's Type Theory: An Introduction. Clarendon Press, Oxford, 1990."},{"key":"20_CR17","unstructured":"E. Palmgreen. A domain interpretation of Martin-L\u00f6f's partial type theories with universes. Technical Report UUDM 1989:11, University of Uppsala, Department of Mathematics, 1989."},{"key":"20_CR18","unstructured":"T. Strahm. Theorien mit Selbst-Applikation. Technical Report IAM-PR-90350, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bern, oct 1990."},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"C. Talcott. A theory for program and data type specification. Theoretical Computer Science, 104(1), Oct. 1992.","DOI":"10.1016\/0304-3975(92)90169-G"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56992-8_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:54Z","timestamp":1605647274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56992-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569923","9783540478904"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-56992-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}