1115 पेपर
यह लघु शोधपत्र लीन (Lean) प्रूफ असिस्टेंट के भीतर इसके प्रमाणों को विश्वसनीय प्रमाणों के रूप में पुनर्गठित करके ऑटोमेटेड थ्योरम प्रवर वैम्पायर (Vampire) में उपयोगकर्ता विश्वास बढ़ाने के चल रहे प्रयासों की रूपरेखा प्रस्तुत करता है।
यह शोध पत्र मल्टी-पार्टिसिपेंट आई/ओ ऑपरेशन्स और एक विशेष सबटाइपिंग रिलेशन को पेश करके, फेडरेटेड लर्निंग प्रोटोकॉल को मॉडल और सत्यापित करने के लिए एसिंक्रोनस बॉटम-अप सेशन टाइपिंग का विस्तार करता है, साथ ही सुरक्षा, डेडलॉक-फ्रीडम, लाइवनेस और सेशन फिडेलिटी को औपचारिक रूप से सिद्ध करता है।
यह शोध पत्र गल्फोंड-स्नाइडर प्रमेय का एक औपचारिक रूप प्रस्तुत करता है, जो लीन 4 (Lean 4) में यह सिद्ध करके हिल्बर्ट की सातवीं समस्या का समाधान करता है कि यदि एक बीजगणितीय संख्या है और एक अपरिमेय बीजगणितीय संख्या है, तो एक अपरिमेय संख्या (transcendental) है।
यह शोध पत्र एक ब्लॉक-पार्टीशन किए गए फाइबोनैकी अनुक्रम का उपयोग करते हुए परिमित स्ट्रिंग्स (finite strings) को प्राकृतिक संख्याओं में एक रैखिक-आकार (linear-size), आक्षेपित (injective) एन्कोडिंग के माध्यम से प्रस्तुत करता है, जो रोस्को की बाइनरी कैरीलेस पेयरिंग पद्धति में निहित घातीय विस्फोट (exponential blowup) से बचते हुए इष्टतम वृद्धि प्राप्त करता है।
यह शोध पत्र प्रदर्शित करता है कि किसी भी बहु-मूल्य वाले फलन (multiple-valued function) को सर्किट-समान और आगमनात्मक (inductive) शैलियों का उपयोग करते हुए एक द्वितीय-क्रम बहुरूपी प्रकार प्रणाली (second-order polymorphic type system) के भीतर रैखिक लैम्ब्डा पदों (linear lambda terms) द्वारा निरूपित किया जा सकता है, जबकि यह अनुकूलन और व्यावहारिक अनुप्रयोगों का भी अन्वेषण करता है।
यह शोध पत्र निर्देशित ग्राफ़ (directed graphs) पर आधारित आइसोले/एचओएल (Isabelle/HOL) प्रूफ़ असिस्टेंट के भीतर नेटवर्क टोपोलॉजी मैट्रिसेस (एडजसेंसी, डिग्री, लैप्लासियन और इंसिडेंस) के एक औपचारिकीकरण को प्रस्तुत करता है, जहाँ क्रोन रिडक्शन (Kron reduction) और पावर डिसिपेशन सत्यापन जैसे उदाहरणों के माध्यम से विद्युत नेटवर्क जैसे सिस्टम के कठोर विश्लेषण का समर्थन करने के लिए शास्त्रीय गुणों और इंटर-मैट्रिक्स संबंधों को सत्यापित किया गया है।
यह शोध पत्र पर रैंक वाले मोनाड्स (ranked monads) और लोकेल्स (locales) में आंतरिक श्रेणियों (internal categories) के बीच एक प्रतिलोम इडेम्पोटेंट एडजंक्शन (contravariant idempotent adjunction) को प्रस्तुत करके मोनाड्स के लिए एक स्टोन द्वैतता (Stone duality) स्थापित करता है, जो शास्त्रीय स्टोन द्वैतता तक सीमित है और हाइपरएफिन-यूनरी मोनाड्स (hyperaffine-unary monads) को एम्पल लोकेलिक श्रेणियों (ample localic categories) के अनुरूप फिक्स्ड पॉइंट्स के रूप में अभिलक्षणित करता है।
यह शोधपत्र उप-ग्राफों के परिमित जाली (finite lattices of subgraphs) के संदर्भ में नेस्टेड स्थितियों और बाधाओं के औपचारिक रूप के लिए एक नेस्टिंग-मुक्त सामान्य रूप (nesting-free normal form) प्रस्तुत करता है।
यह शोधपत्र टाइप Top के साथ विस्तारित सिस्टम I के एक वेरिएंट का Agda में एक पूर्ण औपचारिकीकरण प्रस्तुत करता है, जिसमें प्रोग्रेस और स्ट्रॉन्ग नॉर्मलाइज़ेशन के औपचारिक प्रमाण शामिल हैं।
यह शोध पत्र लीनियर रिकरेंस सीक्वेंस और पावर्स से जुड़ी अंकगणितीय संरचनाओं के लिए मोनैडिक सेकंड-ऑर्डर थ्योरीज़ की डैसिडेबिलिटी (decidability) की जांच करता है, जो डायनेमिकल सिस्टम्स, नंबर थ्योरी और ऑटोमेटा थ्योरी की तकनीकों को एकीकृत करके नए अनकंडीशनल और कंडिशनल परिणाम स्थापित करता है।