{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:39Z","timestamp":1725471159704},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_33","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"377-391","source":"Crossref","is-referenced-by-count":4,"title":["First-Order Logic with Dependent Types"],"prefix":"10.1007","author":[{"given":"Florian","family":"Rabe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_22","volume-title":"Automata, Languages and Programming","author":"R. Bruni","year":"2003","unstructured":"Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, Springer, Heidelberg (2003)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"CASL User Manual","year":"2004","unstructured":"Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol.\u00a02900. Springer, Heidelberg (2004)"},{"key":"33_CR4","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R. Constable","year":"1986","unstructured":"Constable, R., Allen, S., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J., Smith, S.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Cartmell, J.: Generalized algebraic theories and contextual category. Annals of Pure and Applied Logic\u00a032 (1986)","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol.\u00a04, pp. 65\u201389 (1996)","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Diaconescu, R.: Institution-independent Model Theory (2005)","DOI":"10.1007\/11780274_5"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: Internal type theory. In: TYPES, pp. 120\u2013134 (1995)","DOI":"10.1007\/3-540-61780-9_66"},{"key":"33_CR9","volume-title":"Foundations of Automatic Theorem Proving","author":"J. Gallier","year":"1986","unstructured":"Gallier, J.: Foundations of Automatic Theorem Proving. Wiley, Chichester (1986)"},{"issue":"1","key":"33_CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery\u00a039(1), 95\u2013146 (1992)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"33_CR11","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. In: Goguen, J. (ed.) Applications of Algebraic Specification using OBJ, Cambridge (1993)"},{"key":"33_CR12","doi-asserted-by":"publisher","first-page":"159","DOI":"10.2307\/2267044","volume":"14","author":"L. Henkin","year":"1949","unstructured":"Henkin, L.: The completeness of the first-order functional calculus. Journal of Symbolic Logic\u00a014, 159\u2013166 (1949)","journal-title":"Journal of Symbolic Logic"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: CSL, pp. 427\u2013441 (1994)","DOI":"10.1007\/BFb0022273"},{"key":"33_CR14","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner.","author":"G. Huet","year":"1998","unstructured":"Huet, G., Sa\u00efbi, A.: Constructive category theory. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner., MIT Press, Cambridge (1998)"},{"key":"33_CR15","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0168-0072(94)90009-4","volume":"67","author":"R. Harper","year":"1994","unstructured":"Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Annals of Pure and Applied Logic\u00a067, 113\u2013160 (1994)","journal-title":"Annals of Pure and Applied Logic"},{"key":"33_CR16","unstructured":"Makkai, M.: First order logic with dependent sorts (FOLDS) (Unpublished)"},{"key":"33_CR17","volume-title":"Proceedings of the 1973 Logic Colloquium","author":"P. Martin-L\u00f6f","year":"1974","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: Predicative part. In: Proceedings of the 1973 Logic Colloquium, North-Holland, Amsterdam (1974)"},{"key":"33_CR18","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based theorem proving. In: Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier Science Publishers, Amsterdam (2001)"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"33_CR20","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report SRI-CSL-97-2, SRI International (1997)"},{"key":"33_CR21","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of automated reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Handbook of automated reasoning, pp. 1063\u20131147. Elsevier, Amsterdam (2001)"},{"key":"33_CR22","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-540-45085-6_40","volume-title":"19th International Conference on Automated Deduction","author":"B. Pientka","year":"2003","unstructured":"Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification. In: 19th International Conference on Automated Deduction, pp. 473\u2013487. Springer, Heidelberg (2003)"},{"key":"33_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"33_CR24","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015, 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"33_CR25","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. Seely","year":"1984","unstructured":"Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc.\u00a095, 33\u201348 (1984)","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"33_CR26","first-page":"286","volume-title":"Proceedings of the 15th International Conference on Automated Deduction","author":"C. Sch\u00fcrmann","year":"1996","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Kirchner, C., Kirchner, H. (eds.) Proceedings of the 15th International Conference on Automated Deduction, pp. 286\u2013300. Springer, Heidelberg (1996)"},{"key":"33_CR27","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0304-3975(85)90094-5","volume":"37","author":"A. Tarlecki","year":"1985","unstructured":"Tarlecki, A.: On the existence of free models in abstract algebraic institutions. Theoretical Computer Science\u00a037, 269\u2013301 (1985)","journal-title":"Theoretical Computer Science"},{"key":"33_CR28","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/3-540-61464-8_47","volume-title":"Proceedings of the 7th International Conference on Rewriting Techniques and Applications","author":"R. Virga","year":"1996","unstructured":"Virga, R.: Higher-order superposition for dependent types. In: Ganzinger, H. (ed.) Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pp. 123\u2013137. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:14:34Z","timestamp":1605626074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/11814771_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}