{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:27:18Z","timestamp":1725492438312},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665373"},{"type":"electronic","value":"9783540481676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48167-2_1","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T07:40:19Z","timestamp":1191570019000},"page":"1-18","source":"Crossref","is-referenced-by-count":17,"title":["On Relating Type Theories and Set Theories"],"prefix":"10.1007","author":[{"given":"Peter","family":"Aczel","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Peter Aczel, The Type Theoretic Interpretation of Constructive Set Theory, in: MacIntyre, A., Pacholski, L., Paris, J. (eds), Logic Colloquium\u2019 77, (North Holland, Amsterdam, 1978). pp2, 13, 16","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"1_CR2","unstructured":"Peter Aczel, The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles, in: Troelstra, S. S., van Dalen, D. (eds),The L. E. J. Brouwer Centenary Symposium, (North Holland, Amsterdam, 1982). 2, 16"},{"key":"1_CR3","unstructured":"Peter Aczel, The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions, in: Marcus, R. B. et al. (eds), Logic, Methodology and Philosophy of Science VII, (North Holland, Amsterdam, 1986). 2, 13, 16, 17"},{"key":"1_CR4","unstructured":"Barras et al. The Coq Proof Assistant Reference Manual, Version 6.1 INRIA Technical Report, 1996. 1"},{"key":"1_CR5","unstructured":"Thierry Coquand, Metamathematical Investigations of a Calculus of Constructions. In P. Oddifredi (editor), Logic and Computer Science. Academic Press, 1990. 1"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Peter Dybjer, Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their settheoretic semantics. In Gerard Huet and Gordon Plotkin (editors), Logical Frameworks, pp 280\u2013306, Prentice Hall, 1991. 2","DOI":"10.1017\/CBO9780511569807.012"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory. To appear in The Journal of Symbolic Logic, 1999? 2","DOI":"10.2307\/2586554"},{"key":"1_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TLCA","author":"P. Dybjer","year":"1999","unstructured":"Peter Dybjer and Anton Setzer, A finite axiomatization of inductive-recursive definitions. To appear in Proceedings of TLCA 1999, LNCS. 2"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"364","DOI":"10.2307\/2274509","volume":"53","author":"S. Feferman","year":"1988","unstructured":"Solomon Feferman, Hilbert\u2019s Program Relativised: Proof-Theoretical and Foundational Reductions, Journal of Symbolic Logic, Vol 53, (1988) 364\u2013384. 3","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF01278464","volume":"33","author":"Ed. Griffor","year":"1994","unstructured":"Ed. Griffor and Michael Rathjen, The Strength of some Martin-L\u00f6f type theories, Archiv for Mathematical Logic 33 (1994) 347\u2013385. 2, 16","journal-title":"Archiv for Mathematical Logic"},{"key":"1_CR11","unstructured":"Ed. Griffor and Michael Rathjen, Inaccessibility in Constructive Set Theory and type theory, Technical Report U. U. D. M. 1996:20, Department of Mathematics, Uppsala University. 2, 14, 16"},{"key":"1_CR12","unstructured":"Zhaohui Luo and Randy Pollack, LEGO Proof Development System: User\u2019s Manual, Edinburgh University Computer Science Department Technical Report, ECSLFCS-92-211, 1992. 1"},{"key":"1_CR13","unstructured":"Per Martin-L\u00f6f, Intuitionistic type Theory. Studies in Proof Theory, Bibliopolis, 1984. 1"},{"key":"1_CR14","unstructured":"Michael Rathjen, The Realm of Ordinal Analysis, To appear in S. B. Cooper, J. K. Truss (eds.): Sets and Proofs, Proceedings of the Logic Cooloquium\u2019 97, Cambridge University Press. 3"},{"key":"1_CR15","series-title":"Lect Notes Comput Sci","volume-title":"TACS\u2019 97","author":"B. Werner","year":"1997","unstructured":"Benjamin Werner, Sets in Types, Types in Sets, TACS\u2019 97, LNCS 1281. 1, 2"}],"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-48167-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,27]],"date-time":"2020-04-27T01:43:43Z","timestamp":1587951823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48167-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665373","9783540481676"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-48167-2_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}