I gave a brief talk today on the quotation work I'd been doing in MetaCoq, here is the slide deck for anyone interested.
was there an obvious reason for the "else" on slide 3 in Agda? (Interested in if this was due to Agda features or someone had done previous work)
@Karl Palmskog What do you mean "the 'else' on slide 3"? (I don't quite understand the question.)
What I have in Agda (from another project I was working on) is a formalization of Löb's Theorem from an abstract category of syntax based on a generalization of Lawvere's fixpoint theorem. This is sort-of the complement of the work in MetaCoq: a proof of Löb's Theorem that does not commit to a particular AST but tries to be more-or-less compatible with any tree you might pick. There's a rough sketch of the (non-reduction) building blocks / assumptions on slides 9--12, though the Agda source is a more complete (if a bit less readable) list.
The assumptions fall into one of four categories:
(□ A × □ B) → □(A × B)
)Does this answer your question?
I was referring to the "Everything else is comparatively straightforward; details (and Agda formalization) available", yes. So you answered my question with the Agda link, thanks.
Last updated: Oct 13 2024 at 01:02 UTC