Jacques: Created page with "Proof assistants based off of dependent types all use roughly the same core calculi, but use a variety of implementation strategies for their front-ends. To compare and constrast the performance of these systems, we have developed \emph{Panbench}, an extensible DSL for generating programs of increasing size for Agda 2, Rocq, Lean 4, and Idris 2. In this talk, I will discuss the design of the Panbench DSL, and detail a refinement of tagless embeddings used to encode it in..."

2026-10-09T19:08:54Z

Created page with "Proof assistants based off of dependent types all use roughly the same core calculi, but use a variety of implementation strategies for their front-ends. To compare and constrast the performance of these systems, we have developed \emph{Panbench}, an extensible DSL for generating programs of increasing size for Agda 2, Rocq, Lean 4, and Idris 2. In this talk, I will discuss the design of the Panbench DSL, and detail a refinement of tagless embeddings used to encode it in..."

New page

Proof assistants based off of dependent types all use roughly the same
core calculi, but use a variety of implementation strategies for their
front-ends. To compare and constrast the performance of these systems,
we have developed \emph{Panbench}, an extensible DSL for generating programs
of increasing size for Agda 2, Rocq, Lean 4, and Idris 2. In this talk, I will
discuss the design of the Panbench DSL, and detail a refinement of tagless embeddings used to encode it in Haskell.

WG211/M26Mullanix - Revision history