{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T23:52:08Z","timestamp":1648684328113},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631729","type":"print"},{"value":"9783540692010","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63172-0_38","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:15:34Z","timestamp":1330298134000},"page":"167-181","source":"Crossref","is-referenced-by-count":1,"title":["Extending models of second order predicate logic to models of second order dependent type theory"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"10_CR1","unstructured":"H.P. Barendregt, The lambda calculus: its syntax and semantics, revised edition. Studies in Logic and the Foundations of Mathematics, North Holland."},{"key":"10_CR2","unstructured":"H.P. Barendregt, Typed lambda calculi. In Handbook of Logic in Computer Science, eds. Abramski et al., Oxford Univ. Press."},{"key":"10_CR3","unstructured":"S. Berardi, Type dependence and constructive mathematics, Ph.D. thesis, Universita di Torino, Italy."},{"key":"10_CR4","unstructured":"S. Berardi, Encoding of data types in Pure Construction Calculus: a semantic justification, in Logical Environments, eds. G. Huet and G. Plotkin, Cambridge University Press, pp 30\u201360."},{"key":"10_CR5","unstructured":"Th. Coquand, Metamathematical investigations of a calculus of constructions. In Logic and Computer Science, ed. P.G. Odifreddi, APIC series, vol. 31, Academic Press, pp 91\u2013122."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G. Huet, The calculus of constructions, Information and Computation, 76, pp 95\u2013120.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"10_CR7","unstructured":"D. van Dalen, Logic and Structure, third edition. Springer Verlag."},{"key":"10_CR8","unstructured":"J.H. Geuvers, Logics and Type systems, PhD. Thesis, University of Nijmegen, Netherlands."},{"key":"10_CR9","unstructured":"J.H. Geuvers, The Calculus of Constructions and Higher Order Logic, in The Curry-Howard isomorphism, ed. Ph. de Groote, Volume 8 of the \u201cCahiers du Centre de logique\u201d (Universit\u00e9 catholique de Louvain), Academia, Louvain-la-Neuve (Belgium), pp. 139\u2013191."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"M. Stefanova and J.H. Geuvers, A simple semantics for the Calculus of Constructions, to appear in the Proceedings of the ESPRIT-BRA \u2018Types\u2019 meeting, Turin, Italy, 1995.","DOI":"10.1007\/3-540-61780-9_74"},{"key":"10_CR11","unstructured":"J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Camb. Tracts in Theoretical Computer Science 7, Cambridge University Press."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"R. Harper, F. Honsell and G. Plotkin, A framework for defining logics. Proceedings Second Symposium on Logic in Computer Science, (Ithaca, N.Y.), IEEE, Washington DC, pp 194\u2013204.","DOI":"10.1145\/138027.138060"},{"key":"10_CR13","unstructured":"W.A. Howard, The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J.P. Seldin, J.R. Hindley, AcademicPress, New York, pp 479\u2013490."},{"key":"10_CR14","unstructured":"G. Longo and E. Moggi, Constructive Natural Deduction and its \u201cModest\u201d Interpretation. Report CMU-CS-88-131."},{"key":"10_CR15","series-title":"Volume 133 in Studies in Logic and the Foundations of Mathematics","first-page":"1024","volume-title":"Selected Papers on Automath","year":"1994","unstructured":"R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer (editors), Selected Papers on Automath, Volume 133 in Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1994, pp 1024."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"T. Streicher, Independence of the induction principle and the axiom of choice in the pure calculus of constructions, TCS 103(2), pp 395\u2013409.","DOI":"10.1016\/0304-3975(92)90021-7"}],"container-title":["Computer Science Logic","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63172-0_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:02Z","timestamp":1605647822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63172-0_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631729","9783540692010"],"references-count":16,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-63172-0_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1997]]}}}