[Agda] Mechanized semantics of constraint/logic programming languages

Discussion:

a.j.rouvoet

2018-09-20 11:18:03 UTC

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

Bas Spitters

2018-09-20 11:24:45 UTC

Permalink

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

Post by a.j.rouvoet
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
https://lists.chalmers.se/mailman/listinfo/agda

Gabriel Scherer

2018-09-20 12:22:50 UTC

Permalink

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

Post by 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

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda