The POPLmark Challenge is a concrete set of benchmarks intended both for measuring progress and for stimulating discussion and collaboration in mechanizing the metatheory of programming languages. Since work on the challenge problems has died down, the POPLmark wiki has been replaced with this static page recording the submitted solutions and the project’s history.

References in zbMATH (referenced in 38 articles , 1 standard article )

Showing results 1 to 20 of 38.
Sorted by year (citations)

1 2 next

  1. Grohne, Helmut; Voigtländer, Janis: Formalizing semantic bidirectionalization and extensions with dependent types (2017)
  2. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  3. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
  4. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  5. Ciaffaglione, Alberto; Scagnetto, Ivan: Mechanizing type environments in weak HOAS (2015)
  6. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  7. Clouston, Ranald: Nominal Lawvere theories: a category theoretic account of equational theories with names (2014)
  8. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  9. Ahrens, Benedikt: Initiality for typed syntax and semantics (2012)
  10. Appel, Andrew W.; Dockins, Robert; Leroy, Xavier: A list-machine benchmark for mechanized metatheory (2012)
  11. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: Formal metatheory of programming languages in the Matita interactive theorem prover (2012)
  12. Berghofer, Stefan: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (2012)
  13. Charguéraud, Arthur: The locally nameless representation (2012)
  14. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  15. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  16. Hirschowitz, André; Maggesi, Marco: Nested abstract syntax in Coq (2012)
  17. Lee, Gyesik; Oliveira, Bruno C.D.S.; Cho, Sungkeun; Yi, Kwangkeun: GMeta: a generic formal metatheory framework for first-order representations (2012)
  18. Vouillon, Jér^ome: A solution to the PoplMark challenge based on de Bruijn indices (2012)
  19. Stump, Aaron; Kimmell, Garrin; El Haj Omar, Roba: Type preservation as a confluence problem (2011)
  20. Felty, Amy; Pientka, Brigitte: Reasoning with higher-order abstract syntax and contexts: a comparison (2010)

1 2 next