POPLmark challenge
પ્રોગ્રામિંગ લેંગ્વેજ થિયરીમાં, પી. ઓ. પી. એલ. માર્ક ચેલેન્જ ("પ્રોગ્રામિંગ લેંગ્વેજ બેંચમાર્કના સિદ્ધાંતો" માંથી, અગાઉ લોકો માટે મિકેનાઇઝ્ડ મેટાથિયરી!) (આયડેમિર, 2005) એ બેન્ચમાર્કનો સમૂહ છે જે પ્રોગ્રામિંગ ભાષાઓના મેટાથિયરીમાં સ્વચાલિત તર્ક (અથવા યાંત્રીકરણ) ની સ્થિતિનું મૂલ્યાંકન કરવા અને ઔપચારિક પદ્ધતિઓના સમુદાયના વિવિધ ક્રોસ સેક્શનમાં ચર્ચા અને સહયોગને ઉત્તેજીત કરવા માટે રચાયેલ છે. ખૂબ જ ઢીલી રીતે કહીએ તો, પડકાર એ માપવા વિશે છે કે કાર્યક્રમો કેવી રીતે વર્તવાનો હેતુ ધરાવે છે (અને તેમાં સમાવિષ્ટ ઘણા જટિલ મુદ્દાઓ) તેના સ્પષ્ટીકરણ સાથે મેળ કરવા માટે કેટલી સારી રીતે સાબિત થઈ શકે છે. આ પડકાર શરૂઆતમાં યુનિવર્સિટી ઓફ પેન્સિલવેનિયામાં પી. એલ. ક્લબના સભ્યો દ્વારા વિશ્વભરના સહયોગીઓના સહયોગથી રજૂ કરવામાં આવ્યો હતો. મિકેનાઈઝ્ડ મેટાથેરરી પરની વર્કશોપ એ પડકારમાં ભાગ લેનારા સંશોધકોની મુખ્ય બેઠક છે. પી. ઓ. પી. એલ. માર્ક બેન્ચમાર્કની રચના પ્રોગ્રામિંગ ભાષાઓ વિશેના તર્ક માટે સામાન્ય સુવિધાઓ દ્વારા સંચાલિત થાય છે. પડકારની સમસ્યાઓને મોટી પ્રોગ્રામિંગ ભાષાઓના ઔપચારિકરણની જરૂર નથી, પરંતુ તેમને આ વિશે તર્કમાં અભિજાત્યપણાની જરૂર છેઃ બંધનકર્તા મોટાભાગની પ્રોગ્રામિંગ ભાષાઓમાં બંધનકર્તાના અમુક સ્વરૂપો હોય છે, જેમાં ફક્ત ટાઇપ કરેલા લેમ્બડા કલનનાં સરળ બંધનકર્તાઓથી લઈને જટિલ, સંભવિત રીતે રેકોર્ડ પેટર્નની સારવારમાં જરૂરી અનંત બંધનકર્તા સુધીની જટિલતા હોય છે. વિષયમાં ઘટાડો અને મજબૂત સામાન્યીકરણ જેવા ઇન્ડક્શન ગુણધર્મોને ઘણીવાર જટિલ ઇન્ડક્શન દલીલોની જરૂર પડે છે. સહયોગને આગળ વધારવો એ પડકારનો મુખ્ય ઉદ્દેશ હોવાથી, ઉકેલોમાં ફરીથી વાપરી શકાય તેવા ઘટકો હોવાની અપેક્ષા છે જે સંશોધકોને દર વખતે શરૂઆતથી શરૂ કરવાની જરૂર વગર ભાષાની સુવિધાઓ અને ડિઝાઇન શેર કરવાની મંજૂરી આપશે. સમસ્યાઓ, પી. ઓ. પી. એલ. માર્ક પડકાર ત્રણ ભાગોથી બનેલો છે. ભાગ 1 ફક્ત સિસ્ટમ એફ <: (સબટાઇપિંગ સાથે સિસ્ટમ એફ) ના પ્રકારો સાથે સંબંધિત છે, અને તેમાં આવી સમસ્યાઓ છેઃ ટાઇપ સિસ્ટમ સબટાઇપિંગની સંક્રમણશીલતાને સ્વીકારે છે કે કેમ તે તપાસવું. રેકોર્ડ્સની હાજરીમાં સબટાઇપિંગની સંક્રમણક્ષમતાની તપાસ કરવી ભાગ 2 સિસ્ટમ F <: ના વાક્યરચના અને શબ્દાર્થ સાથે સંબંધિત છે. તે શુદ્ધ ટુકડા માટે પ્રકાર સલામતીના પુરાવાઓ સાથે સંબંધિત છે પેટર્ન મેળ ખાતી હાજરીમાં પ્રકાર સલામતી ભાગ 3 સિસ્ટમ એફ <: ની ઔપચારિકતાની ઉપયોગીતા સાથે સંબંધિત છે. ખાસ કરીને, પડકાર માટે પૂછવામાં આવે છેઃ ઔપચારિકરણોમાંથી ઉપયોગી અલ્ગોરિધમ્સ બહાર કાઢીને ઓપરેશનલ સિમેન્ટિક્સનું અનુકરણ અને એનિમેશન નીચેના સાધનોનો ઉપયોગ કરીને પી. ઓ. પી. એલ. માર્ક પડકારના ભાગો માટે ઘણા ઉકેલો પ્રસ્તાવિત કરવામાં આવ્યા છેઃ ઇસાબેલ/એચ. ઓ. એલ., ટ્વેલ્ફ, કોક, αપ્રોલોજ, એ. ટી. એસ., અબેલા અને મેટિટા. એક્સપ્રેશન પ્રોબ્લેમ ક્યુ. ઇ. ડી. મેનિફેસ્ટો પી. ઓ. પી. એલ. પરિષદ સંદર્ભો બ્રાયન ઇ. આયડેમિર, એરોન બોહનન, મેથ્યુ ફેરબેરન, જે. નાથન ફોસ્ટર, બેન્જામિન સી. પિયર્સ, પીટર સેવેલ, દિમિત્રીઓસ વાઇટીનીઓટિસ, જ્યોફ્રી વૉશબર્ન, સ્ટેફની સી. વેઇરીચ અને સ્ટીફન એ. ઝ્ડેન્સવિક પણ જુઓ. લોકો માટે યાંત્રીકૃત મેટાથેરીઃ પી. ઓ. પી. એલ. માર્ક પડકાર. થિયરમ પ્રોવિંગ ઇન હાયર ઓર્ડર લોજિક્સમાં, 18મી આંતરરાષ્ટ્રીય પરિષદ, TPHOLs 2005, કોમ્પ્યુટર સાયન્સમાં વ્યાખ્યાન નોંધોની વોલ્યુમ 3603, પૃષ્ઠો 50-65. સ્પ્રિંગર, બર્લિન/હીડલબર્ગ/ન્યૂયોર્ક, 2005. બેન્જામિન સી. પિયર્સ, પીટર સેવેલ, સ્ટેફની વેઇરીચ, સ્ટીવ ઝ્ડેન્સવિક, ઇટ ઇઝ ટાઇમ ટુ મિકેનાઇઝ પ્રોગ્રામિંગ લેંગ્વેજ મેટાથિયરી, ઇન બર્ટ્રાન્ડ મેયર, જિમ વુડકોક (એડ.) ચકાસાયેલ સોફ્ટવેરઃ સિદ્ધાંતો, સાધનો, પ્રયોગો, LNCS 4171, સ્પ્રિંગર બર્લિન/હીડલબર્ગ, 2008, pp. 26-30, બાહ્ય કડીઓ પી. ઓ. પી. એલ. માર્ક ચેલેન્જ ઔપચારિક પદ્ધતિઓ પ્રોગ્રામિંગ લેંગ્વેજ થિયરી ઓટોમેટેડ થીયરમ પ્રૂવિંગ બેન્ચમાર્ક્સ (કમ્પ્યુટિંગ)