POPLmark utmaning

I programmeringsspråksteori är POPLmark -utmaningen (från "Principles of Programming Languages benchmark", tidigare Mechanized Metatheory for the Masses! ) (Aydemir, 2005) en uppsättning riktmärken utformade för att utvärdera tillståndet för automatiserat resonemang (eller mekanisering) i metateori av programmeringsspråk, och för att stimulera diskussion och samarbete mellan en mångsidig tvärsektion av den formella metodgemenskapen . Mycket löst sett handlar utmaningen om att mäta hur väl program kan bevisas matcha en specifikation av hur de är tänkta att bete sig (och de många komplexa frågor som detta innebär). Utmaningen föreslogs ursprungligen av medlemmarna i PL-klubben vid University of Pennsylvania , i samarbete med medarbetare runt om i världen. Workshop on Mechanized Metatheory är huvudmötet för forskare som deltar i utmaningen.

Utformningen av POPLmark-riktmärket styrs av egenskaper som är gemensamma för resonemang om programmeringsspråk. Utmaningsproblemen kräver inte formalisering av stora programmeringsspråk, men de kräver sofistikerade resonemang om:

Bindning: De flesta programmeringsspråk har någon form av bindning, som sträcker sig i komplexitet från de enkla bindemedlen av enkelt skrivna lambdakalkyler till komplexa, potentiellt oändliga bindemedel som behövs för behandling av postmönster .
Induktionsegenskaper: som subjektsreduktion och stark normalisering kräver ofta komplexa induktionsargument.
Återanvändning För: att ytterligare samarbete är ett centralt syfte med utmaningen, förväntas lösningarna innehålla återanvändbara komponenter som gör det möjligt för forskare att dela språkegenskaper och design utan att kräva att de börjar från början varje gång.

Problemen

Från och med 2007 består POPLmark-utmaningen av tre delar. Del 1 berör endast typerna av System F _<: ( System F med subtyping ), och har problem som:

Kontrollera att typsystemet tillåter transitivitet av subtypning.
Kontrollera transitiviteten av subtyping i närvaro av poster

Del 2 handlar om syntax och semantik för System F _<: . Det handlar om bevis på

Typsäkerhet för det rena fragmentet
Skriv säkerhet i närvaro av mönstermatchning

Del 3 handlar om användbarheten av formaliseringen av System F _<: . Utmaningen kräver särskilt:

Simulera och animera den operativa semantiken
Extrahera användbara algoritmer från formaliseringarna

Flera lösningar har föreslagits för delar av POPLmark-utmaningen, med hjälp av följande verktyg: Isabelle/HOL , Twelf , Coq , αProlog , ATS , Abella och Matita .

Se även

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce , Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie C. Weirich och Stephan A. Zdancewic. Mekaniserad metateori för massorna: POPLmark-utmaningen. I Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, volym 3603 av Lecture Notes in Computer Science, sidorna 50–65. Springer, Berlin/ Heidelberg/ New York, 2005.
Benjamin C. Pierce , Peter Sewell, Stephanie Weirich , Steve Zdancewic, It Is Time to Mechanize Programming Language Metatheory , In Bertrand Meyer, Jim Woodcock (Eds.) Verified Software: Theories, Tools, Experiments , LNCS 4171, Springer Berlin / Heidelberg, 2008, s. 26–30, ISBN 978-3-540-69147-1

externa länkar

POPLmark Challenge