Výzva POPLmark - POPLmark challenge - Wikipedia

Tento článek má několik problémů. Prosím pomozte vylepši to nebo diskutovat o těchto otázkách na internetu diskusní stránka. (Zjistěte, jak a kdy tyto zprávy ze šablony odebrat) tento článek potřebuje další citace pro ověření. Prosím pomozte vylepšit tento článek podle přidávání citací ke spolehlivým zdrojům. Zdroj bez zdroje může být napaden a odstraněn. Najít zdroje: „POPLmark challenge“  – zprávy  · noviny  · knihy  · učenec  · JSTOR (Ledna 2011) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) Tento článek obsahuje a seznam doporučení, související čtení nebo externí odkazy, ale jeho zdroje zůstávají nejasné, protože mu chybí vložené citace. Prosím pomozte zlepšit tento článek představuji přesnější citace. (Ledna 2011) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) (Zjistěte, jak a kdy odstranit tuto zprávu šablony)

v teorie programovacího jazyka, Výzva POPLmark (z „Principles of Programming Languages ​​benchmark“, dříve Mechanizovaná metateorie pro masy!) (Aydemir, 2005) je sada měřítka určené k vyhodnocení stavu automatické uvažování (nebo mechanizace) v metateorie programovacích jazyků a stimulovat diskusi a spolupráci mezi různými průřezy EU formální metody společenství. Velmi volně řečeno, výzvou je měření toho, jak dobře lze prokázat, že programy odpovídají specifikaci toho, jak se mají chovat (a mnoha složitým problémům, které to zahrnuje). Výzvu původně navrhli členové PL klub na University of Pennsylvania ve spolupráci se spolupracovníky z celého světa. The Workshop o mechanizované metateorii je hlavní setkání výzkumných pracovníků účastnících se výzvy.

Návrh benchmarku POPLmark se řídí funkcemi běžnými pro uvažování o programovacích jazycích. Problémy s výzvou nevyžadují formalizaci velkých programovacích jazyků, vyžadují však složitost uvažování o:

Vazba

Většina programovacích jazyků má nějakou formu vazby, jejíž složitost sahá od jednoduchých vazačů jazyka jednoduše zadaný lambda kalkul na komplexní, potenciálně nekonečná pojiva potřebná při léčbě záznam vzory.

Indukce

Vlastnosti jako redukce subjektu a silná normalizace často vyžadují složité indukční argumenty.

Znovu použít

Očekává se, že další spolupráce, která bude klíčovým cílem této výzvy, bude obsahovat opakovaně použitelné komponenty, které by výzkumníkům umožnily sdílet jazykové funkce a návrhy, aniž by bylo nutné pokaždé začít od nuly.

Problémy

Tato část musí být aktualizováno. Aktualizujte prosím tento článek, aby odrážel nedávné události nebo nově dostupné informace. (Březen 2020)

Od roku 2007^{[Aktualizace]}, výzva POPLmark se skládá ze tří částí. Část 1 se týká pouze typů Systém F_<: (Systém F s podtypování ), a má problémy jako:

1. Kontrola, zda to typový systém připouští tranzitivita subtypizace.
2. Kontrola přechodnosti subtypizace za přítomnosti evidence

Část 2 se týká syntaxe a sémantiky systému F._<:. Týká se důkazů o

1. Typ bezpečnosti pro čistý fragment
2. Typ zabezpečení za přítomnosti porovnávání vzorů

Část 3 se týká použitelnosti formalizace systému F._<:. Výzva požaduje zejména:

1. Simulace a animace operační sémantika
2. Extrakce užitečných algoritmů z formalizace

Pro části výzvy POPLmark bylo navrženo několik řešení pomocí následujících nástrojů: Isabelle / HOL, Twelf, Coq, αProlog, ATS, Abella a Matita.

Viz také

• Problém s výrazem
• Manifest QED
• POPL konference

Reference

• Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie C. Weirich a Stephan A. Zdancewic. Mechanizovaná metateorie pro masy: výzva POPLmark. In Theorem Proving in Higher Order Logics, 18. mezinárodní konference, TPHOLs 2005, svazek 3603 přednášek v informatice, strany 50–65. Springer, Berlín / Heidelberg / New York, 2005.

• Benjamin C. Pierce, Peter Sewell, Stephanie Weirich Steve Zdancewic, Je čas mechanizovat metateorii programovacího jazyka, V Bertrand Meyer, Jim Woodcock (Eds.) Ověřený software: teorie, nástroje, experimenty, LNCS 4171, Springer Berlin / Heidelberg, 2008, s. 26–30, ISBN  978-3-540-69147-1

externí odkazy

• Výzva POPLmark

Tento počítačová věda článek je a pahýl. Wikipedii můžete pomoci pomocí rozšiřovat to.

Tento programovací jazyk související článek je a pahýl. Wikipedii můžete pomoci pomocí rozšiřovat to.