[Agda] Mechanized semantics of constraint/logic programming languages

[Gabriel Scherer]

Stefania Dumbrava has worked on verified Datalog engines, with and
without negation, in Coq.

  Certifying Standard and Stratified Datalog Inference Engines in SSReflect
  Véronique Benzaken, Évelyne Contejean, Stefania Dumbrava, 2017
  https://hal.archives-ouvertes.fr/hal-01745566/

PhD thesis:

  A Coq Formalization of Relational and Deductive Databases - and
Mechanization of Datalog
  Stefania Dumbrava, 2016
  https://tel.archives-ouvertes.fr/tel-01534575




On Thu, Sep 20, 2018 at 1:25 PM Bas Spitters <b.a.w.spitters at gmail.com> wrote:
>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda