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 48 articles , 1 standard article )

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

1 2 3 next

  1. Carette, Jacques; Farmer, William M.: Formalizing mathematical knowledge as a biform theory graph: a case study (2017)
  2. Cheney, James; Momigliano, Alberto: $\alpha\mathrmCheck$: a mechanized metatheory model checker (2017)
  3. Grohne, Helmut; Voigtländer, Janis: Formalizing semantic bidirectionalization and extensions with dependent types (2017)
  4. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  5. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
  6. Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
  7. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  8. Ciaffaglione, Alberto; Scagnetto, Ivan: Mechanizing type environments in weak HOAS (2015)
  9. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
  10. Clouston, Ranald: Nominal Lawvere theories: a category theoretic account of equational theories with names (2014)
  11. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  12. Smetsers, Sjaak; Barendsen, Erik: Verifying functional formalizations -- a type-theoretical case study in PVS (2013)
  13. Ahrens, Benedikt: Initiality for typed syntax and semantics (2012)
  14. Appel, Andrew W.; Dockins, Robert; Leroy, Xavier: A list-machine benchmark for mechanized metatheory (2012)
  15. Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico: Formal metatheory of programming languages in the Matita interactive theorem prover (2012)
  16. Berghofer, Stefan: A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (2012)
  17. Charguéraud, Arthur: The locally nameless representation (2012)
  18. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  19. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  20. Hirschowitz, André; Maggesi, Marco: Nested abstract syntax in Coq (2012)

1 2 3 next