Stream: Coq users

Topic: Shallow embedding of separation logic and custom entailment


view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 10:23):

You can also just use reification inside tactics — basically, you can analyze formulas in Ltac(1/2) or other tactic languages.

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 10:31):

That lets you convert formulas from a shallow to a deep embedding; however, in this scenario there's no need for a deep embedding of derivations

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 10:33):

I think the Diaframe automation for Iris implements quite a lot directly using typeclass inference, which doesn't even need a deep embedding

view this post on Zulip towokit928 (Sep 12 2023 at 01:56):

Thanks! Do you know of examples of how to perform this conversion using Ltac?

I was thinking of proving soundness of the entailment procedure too - would that be doable for a procedure written in Ltac?

view this post on Zulip Paolo Giarrusso (Sep 12 2023 at 04:21):

http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html is an introduction to proof by reflection. While for instance https://arxiv.org/abs/1102.1323 Sec. 9 shows how to achieve quoting using typeclass search.

view this post on Zulip Paolo Giarrusso (Sep 12 2023 at 04:25):

You can't do proofs about Ltac, but to prove entailment correct, you can still write it in Coq — only "reification" must happen via metaprogramming.

Concretely, once you have quoted your shallowly embedded goal g to a deeply embedded goal G such that eval G = g, you _can_ perform your transformation via a _Coq_ (Gallina) function f : tactic transforming the goal to a new one — for instance you could define tactic as ∀ G : Goal, { newG | eval newG -> eval G }.

view this post on Zulip towokit928 (Sep 12 2023 at 06:24):

Thanks, will check those out!

view this post on Zulip Paolo Giarrusso (Sep 12 2023 at 13:06):

@towokit928 also you _might_ be interested in https://iris-project.org/ — the Iris separation logic framework is very flexible, its engineering is pretty robust, and the ecosystem includes projects on automation like Diaframe. But probably less appropriate if you want a minimal system.

view this post on Zulip Karl Palmskog (Sep 12 2023 at 13:07):

Foundations of separation logic teaching material links: https://chargueraud.org/teach/verif/


Last updated: Jun 23 2024 at 05:02 UTC