POPLMARK挑战
在编程语言理论中， Poplmark挑战（来自“编程语言原理基准”，以前是群众的机械化元看！ ）（Aydemir，2005年）是一组旨在评估自动推理（或机械化）状态的基准测试。对编程语言的元看，并激发正式方法社区的各种横截面之间的讨论和协作。非常宽松地说，挑战是关于如何证明程序可以证明其打算如何行为的规范的方法（以及这涉及的许多复杂问题）。挑战最初是由宾夕法尼亚大学PL俱乐部成员与世界各地的合作者联合提出的。机械化元心理的研讨会是参加挑战的研究人员的主要会议。
Poplmark基准测试的设计由有关编程语言的推理所共有的功能指导。挑战问题不需要大型编程语言的形式化，但是它们确实需要进行精致：
- 捆绑
- 大多数编程语言具有某种形式的结合，从简单键入的lambda演算的简单粘合剂到复杂的，潜在的无限粘合剂的复杂性，在治疗记录模式中所需的无限粘合剂。
- 就职
- 诸如降低受试者和强范围的属性通常需要复杂的诱导参数。
- 重用
- 进一步的协作是挑战的关键目的，这些解决方案有望包含可重复使用的组件，这些组件将使研究人员能够共享语言功能和设计而无需每次从头开始。
问题
截至2007年，Poplmark挑战由三个部分组成。第1部分仅关注系统f <：（系统f ）的类型，并且存在诸如：
第2部分涉及系统f <：的语法和语义。它涉及证明
第3部分涉及系统f <：。特别是，挑战要求：
- 模拟和动画操作语义
- 从形式上提取有用的算法
使用以下工具： Isabelle/Hol ， Twelf ， Coq ， αProlog ， ATS ， Abella和Matita提出了一些针对Poplmark挑战部分的解决方案。