POPLmark challenge
प्रोग्रामिंग भाषा सिद्धांत में, पी. ओ. पी. एल. मार्क चुनौती ("प्रोग्रामिंग भाषाओं के मानदंड के सिद्धांतों" से, पूर्व में जनसमूह के लिए मशीनीकृत मेटाथियरी!) (आयडेमिर, 2005) मानकों का एक समूह है जिसे प्रोग्रामिंग भाषाओं के मेटाथियरी में स्वचालित तर्क (या मशीनीकरण) की स्थिति का मूल्यांकन करने और औपचारिक तरीकों के समुदाय के विविध क्रॉस सेक्शन के बीच चर्चा और सहयोग को प्रोत्साहित करने के लिए डिज़ाइन किया गया है। बहुत शिथिल रूप से बोलते हुए, चुनौती इस बात के मापन के बारे में है कि कार्यक्रमों को कैसे व्यवहार करने का इरादा है (और इसमें शामिल कई जटिल मुद्दे) के विनिर्देश से मेल खाने के लिए कितनी अच्छी तरह से साबित किया जा सकता है। इस चुनौती को शुरू में पेंसिल्वेनिया विश्वविद्यालय में पी. एल. क्लब के सदस्यों द्वारा दुनिया भर के सहयोगियों के सहयोग से प्रस्तावित किया गया था। मशीनीकृत मेटाथियरी पर कार्यशाला चुनौती में भाग लेने वाले शोधकर्ताओं की मुख्य बैठक है। पी. ओ. पी. एल. मार्क. मानक की रूपरेखा प्रोग्रामिंग भाषाओं के बारे में तर्क करने के लिए सामान्य विशेषताओं द्वारा निर्देशित होती है। चुनौती की समस्याओं के लिए बड़ी प्रोग्रामिंग भाषाओं के औपचारिकरण की आवश्यकता नहीं होती है, लेकिन उन्हें इस बारे में तर्क करने में परिष्कार की आवश्यकता होती हैः बाइंडिंग अधिकांश प्रोग्रामिंग भाषाओं में बाइंडिंग के कुछ रूप होते हैं, जो जटिलता में केवल टाइप किए गए लैम्ब्डा कलन के सरल बाइंडर से लेकर जटिल, संभावित रूप से रिकॉर्ड पैटर्न के उपचार में आवश्यक अनंत बाइंडर तक होते हैं। विषय में कमी और मजबूत सामान्यीकरण जैसे प्रेरण गुणों के लिए अक्सर जटिल प्रेरण तर्कों की आवश्यकता होती है। सहयोग को आगे बढ़ाना चुनौती का एक प्रमुख उद्देश्य होने के नाते, समाधानों में पुनः प्रयोज्य घटक होने की उम्मीद है जो शोधकर्ताओं को हर बार खरोंच से शुरू करने की आवश्यकता के बिना भाषा की विशेषताओं और डिजाइनों को साझा करने की अनुमति देगा। समस्याएँ, पी. ओ. पी. एल. मार्क चुनौती तीन भागों से बनी है। भाग 1 केवल सिस्टम एफ <: (सबटाइपिंग के साथ सिस्टम एफ) के प्रकारों से संबंधित है, और इसमें इस तरह की समस्याएं हैं जैसे किः यह जांचना कि टाइप सिस्टम सबटाइपिंग की पारगमनशीलता को स्वीकार करता है। अभिलेखों की उपस्थिति में उपप्रकार की पारगमनशीलता की जाँच करना भाग 2 प्रणाली एफ <: के वाक्यविन्यास और शब्दार्थ से संबंधित है। यह शुद्ध टुकड़े के लिए प्रकार सुरक्षा के प्रमाणों से संबंधित है, पैटर्न मिलान भाग 3 की उपस्थिति में प्रकार सुरक्षा प्रणाली एफ <: के औपचारिकरण की उपयोगिता से संबंधित है। विशेष रूप से, चुनौती निम्नलिखित के लिए पूछती हैः औपचारिकरणों से उपयोगी एल्गोरिदम निकालकर परिचालन शब्दार्थ का अनुकरण और एनिमेशन करना निम्नलिखित उपकरणों का उपयोग करके पी. ओ. पी. एल. मार्क चुनौती के कुछ हिस्सों के लिए कई समाधान प्रस्तावित किए गए हैंः इसाबेल/एच. ओ. एल., ट्वेल्फ, सी. ओ. क्यू., αप्रोलॉग, ए. टी. एस., अबेला और मैटिटा। एक्सप्रेशन प्रॉब्लम क्यू. ई. डी. मैनिफेस्टो पी. ओ. पी. एल. सम्मेलन संदर्भ ब्रायन ई. आयडेमिर, आरोन बोहनन, मैथ्यू फेयरबेर्न, जे. नाथन फोस्टर, बेंजामिन सी. पियर्स, पीटर सेवेल, दिमित्रिओस वाइटिनियोटिस, जेफ्री वॉशबर्न, स्टेफनी सी. वेइरिक और स्टीफन ए. जेडान्स्विक भी देखें। जनता के लिए मशीनीकृत मेटाथियोरीः पी. ओ. पी. एल. मार्क चुनौती। थ्योरम प्रोविंग इन हायर ऑर्डर लॉजिक्स में, 18वें अंतर्राष्ट्रीय सम्मेलन, टी. पी. एच. ओ. एल. एस. 2005, खंड 3603 ऑफ लेक्चर नोट्स इन कंप्यूटर साइंस, पृष्ठ 50-65। स्प्रिंगर, बर्लिन/हीडलबर्ग/न्यूयॉर्क, 2005। बेंजामिन सी. पियर्स, पीटर सेवेल, स्टेफनी वेरिच, स्टीव जेडांसविक, इट इज टाइम टू मैकेनाइज प्रोग्रामिंग लैंग्वेज मेटाथियरी, इन बर्ट्रेंड मेयर, जिम वुडकॉक (एड.) सत्यापित सॉफ्टवेयरः सिद्धांत, उपकरण, प्रयोग, एलएनसीएस 4171, स्प्रिंगर बर्लिन/हीडलबर्ग, 2008, पीपी। 26-30, बाहरी लिंक पी. ओ. पी. एल. मार्क. चुनौती औपचारिक तरीके प्रोग्रामिंग भाषा सिद्धांत स्वचालित प्रमेय बेंचमार्क (कंप्यूटिंग) साबित कर रहा है