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

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

1 2 3 4 next

  1. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  2. Siek, Jeremy G.; Chen, Tianyu: Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi (2021)
  3. Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
  4. Chapman, James; Kireev, Roman; Nester, Chad; Wadler, Philip: System F in Agda, for fun and profit (2019)
  5. García-Pérez, Álvaro; Nogueira, Pablo: The full-reducing krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus (2019)
  6. Miller, Dale: Mechanized metatheory revisited (2019)
  7. Cave, Andrew; Pientka, Brigitte: Mechanizing proofs with logical relations -- Kripke-style (2018)
  8. Miquey, Étienne: Formalizing implicative algebras in Coq (2018)
  9. Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom: Formalization of a polymorphic subtyping algorithm (2018)
  10. Carette, Jacques; Farmer, William M.: Formalizing mathematical knowledge as a biform theory graph: a case study (2017)
  11. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  12. Grohne, Helmut; Voigtländer, Janis: Formalizing semantic bidirectionalization and extensions with dependent types (2017)
  13. Kaiser, Jonas; Pientka, Brigitte; Smolka, Gert: Relating system F and (\lambda2): a case study in Coq, Abella and Beluga (2017)
  14. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  15. Haslbeck, Maximilian P. L.; Nipkow, Tobias: Verified analysis of list update algorithms (2016)
  16. Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew: Modular verification of chemical reaction network encodings via serializability analysis (2016)
  17. Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
  18. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  19. Ciaffaglione, Alberto; Scagnetto, Ivan: Mechanizing type environments in weak HOAS (2015)
  20. Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)

1 2 3 4 next