हाल ही में शुरू किया गया डिपेंडेंट टाइप हायर-ऑर्डर लॉजिक (DHOL) अभिव्यक्ति और स्वचालित समर्थन के बीच एक दिलचस्प समझौता प्रदान करता है। यह मानक HOL पर अभिव्यक्ति को बहुत अधिक विस्तारित करने के लिए प्रकार प्रणाली की निर्णायकता का त्याग करता है, जबकि HOL में सही और पूर्ण परिवर्तन के माध्यम से मजबूत स्वचालित प्रमेय सिद्ध करने का समर्थन बनाए रखता है। इस पत्र में, हम परिष्कृत प्रकारों और भागफल प्रकारों के साथ DHOL का विस्तार करने के लिए इस डिज़ाइन का लाभ उठाते हैं। ये दो विशेषताएँ आमतौर पर चिकित्सकों द्वारा अनुरोध की जाती हैं, लेकिन स्वचालित प्रमेय सिद्धकर्ताओं द्वारा शायद ही कभी प्रदान की जाती हैं, क्योंकि उन्हें स्वाभाविक रूप से अनिर्णीत टाइपिंग की आवश्यकता होती है, जिससे उन्हें निर्णायक प्रकार प्रणाली में उलटना बहुत कठिन हो जाता है। हालाँकि, चूँकि DHOL पहले से ही कठिन काम को संभालता है, इसलिए उन्हें जोड़ना न केवल व्यवहार्य है, बल्कि सुरुचिपूर्ण और सीधा भी है। विशेष रूप से, हम उपप्रकारों के विशेष मामलों के रूप में परिष्कृत प्रकार और भागफल प्रकारों को जोड़ते हैं, जो प्रासंगिक विहित समावेशन या प्रक्षेपण मानचित्रों को पहचान मानचित्रों से बदलकर प्रतिनिधित्व में महंगे परिवर्तनों से बचते हैं। हम विस्तारित भाषा के लिए HOL में वाक्यविन्यास, शब्दार्थ और परिवर्तन के साथ-साथ शुद्धता और पूर्णता के प्रमाण प्रस्तुत करते हैं।
