Stream: MetaCoq

Topic: MetaCoq Quotation Slide Deck

view this post on Zulip Jason Gross (Oct 17 2023 at 16:21):

I gave a brief talk today on the quotation work I'd been doing in MetaCoq, here is the slide deck for anyone interested.

view this post on Zulip Karl Palmskog (Oct 17 2023 at 16:57):

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)

view this post on Zulip Jason Gross (Oct 18 2023 at 02:24):

@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:

  1. adding a layer of quotation (what I worked on in MetaCoq)
  2. decidable equality of syntax trees (also done in MetaCoq)
  3. assumptions that are (I claim) obviously straightforward (things like (□ A × □ B) → □(A × B))
  4. assumptions that are about reduction behavior (which I've not thought much about the difficulty of; but these are only needed for establishing that Löb's Theorem produces a fix point (unfortunately this is needed even in the computational part when using the diagonal lemma to discharge some assumptions of Löb's Theorem though))

Does this answer your question?

view this post on Zulip Karl Palmskog (Oct 18 2023 at 06:18):

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: Jul 23 2024 at 21:01 UTC