{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:51:03Z","timestamp":1773096663382,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540680840","type":"print"},{"value":"9783540681038","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68103-8_3","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T04:10:07Z","timestamp":1210047007000},"page":"33-50","source":"Crossref","is-referenced-by-count":2,"title":["Dependently Sorted Logic"],"prefix":"10.1007","author":[{"given":"Jo\u00e3o Filipe","family":"Belo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Gambino, N., Aczel, P.: The generalised type-theoretic intepretation of constructive set theory (preprint 2005)","DOI":"10.2178\/jsl\/1140641163"},{"key":"3_CR2","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a0141. North Holland, Amsterdam (1999)"},{"key":"3_CR3","unstructured":"Aczel, P.: Predicate logic with dependent sorts or types. Unpublished (2004)"},{"key":"3_CR4","unstructured":"Belo, J.F.: Dependently typed predicate logic. Master\u2019s thesis, University of Manchester (2004)"},{"key":"3_CR5","unstructured":"Makkai, M.: First order logic with dependent sorts, with applications to category theory. Unpublished (1995)"},{"key":"3_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/11814771_33","volume-title":"Automated Reasoning","author":"F. Rabe","year":"2006","unstructured":"Rabe, F.: First-order logic with dependent types. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 377\u2013391. Springer, Heidelberg (2006)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)"},{"issue":"4","key":"3_CR8","first-page":"265","volume":"10","author":"M. Benke","year":"2003","unstructured":"Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing\u00a010(4), 265\u2013289 (2003)","journal-title":"Nordic J. of Computing"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-48256-3_5","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Pfeifer","year":"1999","unstructured":"Pfeifer, H., Rue\u00df, H.: Polytypic proof construction. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 55\u201372. Springer, Heidelberg (1999)"},{"key":"3_CR10","unstructured":"Cartmell, J.: Generalized algebraic theories and contextual categories. PhD thesis, Univ. Oxford (1978)"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"Cartmell, J.: Generalized algebraic theories and contextual categories. Ann. Pure Appl. Logic\u00a032, 209\u2013243 (1986)","journal-title":"Ann. Pure Appl. Logic"},{"key":"3_CR12","series-title":"Algebraic and Logical Structures","volume-title":"Handbook of Logic in Computer Science","author":"A.M. Pitts","year":"2000","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. Algebraic and Logical Structures, vol.\u00a05, ch.2, Oxford University Press, Oxford (2000)"},{"key":"3_CR13","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1017\/CBO9780511526619.004","volume-title":"Semantics and Logics of Computation","author":"M. Hofmann","year":"1997","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, vol.\u00a014, pp. 79\u2013130. Cambridge University Press, Cambridge (1997)"},{"key":"3_CR14","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic proof theory","author":"A.S. Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. Cambridge University Press, Cambridge (2000)"},{"key":"3_CR15","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"P.T. Johnstone","year":"2002","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol.\u00a02. Oxford University Press, Oxford (2002)"},{"key":"3_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172066","volume-title":"Notes on Logic and Set Theory","author":"P.T. Johnstone","year":"1987","unstructured":"Johnstone, P.T.: Notes on Logic and Set Theory. Cambridge University Press, Cambridge (1987)"},{"key":"3_CR17","unstructured":"Shoenfield, J.R.: Mathematical Logic. Association for Symbolic Logic (1967)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68103-8_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T04:24:59Z","timestamp":1684383899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68103-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540680840","9783540681038"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68103-8_3","relation":{},"subject":[]}}