{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T10:54:12Z","timestamp":1766400852485,"version":"3.44.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its expressiveness over standard HOL. Yet it retains strong automated theorem proving support via a sound and complete translation to HOL.<\/jats:p>\n          <jats:p>We leverage this design to extend DHOL with refinement and quotient types. Both of these are commonly requested by practitioners but rarely provided by automated theorem provers. This is because they inherently require undecidable typing and thus are very difficult to retrofit to decidable type systems. But with DHOL already doing the heavy lifting, adding them is not only possible but elegant and simple.<\/jats:p>\n          <jats:p>Concretely, we add refinement and quotient types as special cases of subtyping. This turns the associated canonical inclusion resp. projection maps into identity maps and thus avoids costly changes in representation. We present the syntax, semantics, and translation to HOL for the extended language, including the proofs of soundness and completeness.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_6","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:47Z","timestamp":1757887427000},"page":"98-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Subtyping in\u00a0Dependently-Typed Higher-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9751-8989","authenticated-orcid":false,"given":"Colin","family":"Rothgang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"6_CR1","unstructured":"Allen, S.: A non-type-theoretic semantics for type-theoretic language. Ph.D. thesis, Cornell University (1987)"},{"key":"6_CR2","unstructured":"Andrews, P.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press (1986)"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Hewer, B., Hutton, G.: Quotient Haskell: lightweight quotient types for all. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632869","DOI":"10.1145\/3632869"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-20615-8_17","volume-title":"Intelligent Computer Mathematics","author":"G Bancerek","year":"2015","unstructured":"Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261\u2013279. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_17"},{"key":"6_CR5","unstructured":"Rothgang, C., Rabe, F.: Subtyping in DHOL \u2013 Extended preprint (2025). https:\/\/arxiv.org\/abs\/2507.02855"},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"6_CR7","unstructured":"Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall (1986)"},{"key":"6_CR8","unstructured":"Coq Development Team: The Coq Proof Assistant: Reference Manual. Technical report, INRIA (2015)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction \u2013 CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"issue":"3","key":"6_CR10","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0168-0072(93)90144-3","volume":"64","author":"W Farmer","year":"1993","unstructured":"Farmer, W.: A simple type theory with partial functions and subtypes. Ann. Pure Appl. Logic 64(3), 211\u2013240 (1993)","journal-title":"Ann. Pure Appl. Logic"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Gordon, M.: HOL: a proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Kluwer-Academic Publishers (1988)","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11541868_9","volume-title":"Theorem Proving in Higher Order Logics","author":"PV Homeier","year":"2005","unstructured":"Homeier, P.V.: A design structure for higher order quotients. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 130\u2013146. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_9"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_9"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Hurd, J.: Predicate subtyping with predicate sets. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics, pp. 265\u2013280 (2001)","DOI":"10.1007\/3-540-44755-5_19"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-662-54434-1_27","volume-title":"Programming Languages and Systems","author":"O Kun\u010dar","year":"2017","unstructured":"Kun\u010dar, O., Popescu, A.: Comprehending Isabelle\/HOL\u2019s consistency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 724\u2013749. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_27"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: predicative part. In: Proceedings of the 1973 Logic Colloquium, pp. 73\u2013118. North-Holland (1974)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-031-63498-7_6","volume-title":"Automated Reasoning","author":"J Niederhauser","year":"2024","unstructured":"Niederhauser, J., Brown, C., Kaliszyk, C.: Tableaux for automated reasoning in dependently-typed higher-order logic. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Automated Reasoning, pp. 86\u2013104. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_6"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-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. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Popescu, A., Traytel, D.: Admissible types-to-pers relativization in higher-order logic. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571235","DOI":"10.1145\/3571235"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Ranalter, D., Brown, C., Kaliszyk, C.: Experiments with choice in dependently-typed higher-order logic. In: Bj\u00f8rner, N., Heule, M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence and Reasoning, pp. 311\u2013320 (2024)","DOI":"10.29007\/2v8h"},{"key":"6_CR21","unstructured":"Ranalter, D., Rabe, F., Kaliszyk, C.: Polymorphic theorem proving for DHOL"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-031-38499-8_25","volume-title":"Automated Deduction","author":"C Rothgang","year":"2023","unstructured":"Rothgang, C., Rabe, F., Benzm\u00fcller, C.: Theorem proving in dependently typed higher-order logic. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction, pp. 438\u2013455. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_25"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:49Z","timestamp":1757887429000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}