1117 पेपर
यह शोध पत्र क्लासिकल लीनियर लॉजिक के मल्टीप्लिकेटिव-एडिटिव फ्रैगमेंट (MALL) के लिए बेस-एक्सटेंशन सिमेंटिक्स के प्रूफ़-थ्योरेटिक फ्रेमवर्क का विस्तार करता है, जो बेस सपोर्ट के माध्यम से प्रमाणों को अभिलक्षणित करने के लिए एक नवीन दृष्टिकोण प्रस्तुत करता है।
यह शोध पत्र आंशिक और पूर्ण होअर लॉजिक (Hoare logic) और उनके द्वैत, रिवर्स होअर लॉजिक (reverse Hoare logic) दोनों के लिए चक्रीय प्रमाण प्रणालियों (cyclic proof systems) की सुदृढ़ता (soundness) और सापेक्ष पूर्णता (relative completeness) को यह प्रदर्शित करके स्थापित करता है कि वे कैसे स्पष्ट लूप इनवेरिएंट्स (loop invariants) और टर्मिनेशन मेजर्स (termination measures) को क्रमशः सह-आगमनात्मक (coinductive) और आगमनात्मक (inductive) वैश्विक सुदृढ़ता शर्तों द्वारा शासित चक्रीय अनरोलिंग नियमों (cyclic unrolling rules) से प्रतिस्थापित करते हैं।
यह मानते हुए कि बहुपद-आकार के बूलियन सर्किट दो -बिट अभाज्य संख्याओं के गुणनफलों के एक स्थिर अंश को गुणनखंडित नहीं कर सकते, यह शोध पत्र यह प्रदर्शित करता है कि शार्पली बाउंडेड चॉइस (sharply bounded choice) के साथ संवर्धित बाउंडेड अरिथमेटिक थ्योरी , सभी संख्याओं के लिए अभाज्य विभाजकों के अस्तित्व को सिद्ध नहीं कर सकती है, जिससे एक ऐसे मॉडल का अस्तित्व निहित होता है जिसमें एक गैर-मानक संख्या बिना अभाज्य गुणनखंडन के मौजूद है।
यह शोध पत्र संभाव्य सेपरेशन लॉजिक (probabilistic separation logic) का एक सिमेंटिक सूत्रीकरण प्रस्तुत करता है जो सुरक्षा (safety) को विनिर्देशों (specifications) में एकीकृत करके एक सरल, साइड-कंडीशन-मुक्त फ्रेम नियम प्राप्त करता है ताकि सापेक्ष सघनता (relative tightness) के महत्वपूर्ण गुण को स्थापित किया जा सके।
यह शोध पत्र स्थापित करता है कि आंशिक मार्कोव श्रेणियाँ (partial Markov categories) स्वाभाविक रूप से प्रीऑर्डर-संवर्धित (preorder-enriched) होती हैं, कोडायगोनल मानचित्रों (codiagonal maps) और क्रम गुणों (order properties) के बीच संबंध का अन्वेषण करता है, और यह सिद्ध करता है कि अद्यतनीकरण (updating), एक सिंथेटिक कॉची-श्वार्ज़ असमानता (synthetic Cauchy–Schwarz inequality) के माध्यम से वैधता को बढ़ाता है।
यह शोधपत्र होमोटोपी टाइप थ्योरी के भीतर 'क्वोटिएंट इंडक्टिव-इंडक्टिव टाइप्स' (Quotient Inductive-Inductive Types) के रूप में उन्हें परिभाषित करके, बीजगणितीय प्रभावों (algebraic effects) का प्रतिनिधित्व करने वाले प्रारंभिक DCPO बीजगणितों के निर्माण के लिए एक सामान्य ढांचा प्रस्तुत करता है, जो कि क्यूबिकल एगडा (Cubical Agda) में कार्यान्वयित एक औपचारिकीकरण है जो पार्शियलिटी (partiality) और पावर डोमेन (power domains) जैसे विभिन्न डोमेन निर्माणों को एकीकृत करता है।
यह शोधपत्र ब्रांचिंग प्रकारों और मात्रात्मक प्रेडिकेट लिफ्टिंग्स द्वारा पैरामीटराइज्ड फिक्स्पॉइंट मोडल लॉजिक और CTL* के लिए एक कंटीन्यूएशन सिमेंटिक्स प्रस्तुत करता है, जो गैर-अधिकतम निष्पादन मानचित्रों (non-maximal execution maps) का उपयोग करने के लिए CTL* मॉडलों को पुनर्गठित करते हुए और CTL को फिक्स्पॉइंट मोडल लॉजिक में एनकोड करने की शर्तों को स्थापित करते हुए इसके कोएल्जेब्रिक सिमेंटिक्स के साथ इसकी समानता को सिद्ध करता है।
यह शोध पत्र कॉन्फ़िगरेशन संरचनाओं पर एक सममित रेसिडुएशन (residuation) ऑपरेशन का उपयोग करके और प्राइम इवेंट संरचनाओं के लिए एक अर्थविज्ञान (semantics) व्युत्पन्न करके, जो संघर्ष (conflict) और कार्य-कारणता (causality) को द्वैत बनाता है, उत्क्रमणीय गणनाओं (reversible computations) को समाहित करने वाले समवर्तीता के कारणत्मक मॉडलों (causal models) का एक रूढ़िवादी विस्तार प्रस्तावित करता है।
यह शोध पत्र डिकोडेंसिटी मोनाड्स (dicodensity monads) प्रस्तुत करता है, जो स्ट्रॉन्ग डिनैचुरलिटी (strong dinaturality) पर आधारित और पॉलीमॉर्फिक लैम्ब्डा कैलकुलस (polymorphic lambda calculus) से प्रेरित कोडेन्सिटी मोनाड्स का एक सामान्यीकरण है, ताकि होम-फंक्टर्स (hom-functors) और इंटरनलाइज्ड होम-सेट्स (internalized hom-sets) से उत्पन्न होने वाले मोनाड्स के लिए नए लक्षण वर्णन और आइसोमोर्फिज्म स्थितियाँ प्रदान की जा सकें, जिनमें ऑर्डर्ड नॉन-डिटरमिनिस्टिक कंप्यूटेशन्स (ordered nondeterministic computations) को मॉडल करने वाले भी शामिल हैं।
यह शोधपत्र फंक्शनल मशीन कैलकुलस (Functional Machine Calculus) को अनुक्रमिक (sequential) से ब्रांचिंग (branching) और लूपिंग (looping) कंट्रोल फ्लो तक विस्तारित करता है, जो एक मल्टी-स्टैक कृविन मशीन (multi-stack Krivine machine) पर आधारित एक एकीकृत परिचालन अर्थविज्ञान (unified operational semantics) के माध्यम से कन्फ्लुएंट रिडक्शन (confluent reduction), स्ट्रॉन्ग नॉर्मलाइजेशन (strong normalization) जैसी प्रमुख विशेषताओं को संरक्षित करते हुए एक पूर्ण इमपेरेटिव भाषा (imperative language) के निष्ठापूर्ण एम्बेडिंग को सक्षम बनाता है।