[Agda] Mechanized semantics of constraint/logic programming languages

[Bas Spitters]

Not sure whether this is what you are looking for, but there's some
interesting work around using /-prolog in the context of type theory.
E.g.
https://github.com/LPCIC/coq-elpi
On Thu, Sep 20, 2018 at 1:18 PM a.j.rouvoet <a.j.rouvoet at gmail.com> wrote:
>
> Dear all,
>
> Does anyone know of mechanized operational semantics for
> constraint/logic programming languages?
> I am interested in mechanized semantic (in Agda/Coq/...) for anything
> from ML constraints, to CHR, to Prolog and friends.
>
> Thank you,
>
>
> Arjen Rouvoet
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda