## Stream: MetaCoq

### Topic: MetaCoq Quotation Slide Deck

#### 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.

#### 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)

#### 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?

#### 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