Email Gateway (Aug 18 2022 at 09:49): Email Gateway (Aug 18 2022 at 09:49):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
I'm starting a project to formalize some aspects of a mini-Prolog,
and was
wondering if there has been any work done on formalizing logic
programming,
besides the unification algorithm. I found one paper from TPHOL '01,
but my
library doesn't have that edition:
Refinement Calculus for Logic Programming in Isabelle/HOL, by
Heymer, et. al.
Thanks,
Sean
Email Gateway (Aug 18 2022 at 09:49):From: Tobias Nipkow <nipkow@in.tum.de>
This could be of interest:
Cornelia Pusch: Verification of Compiler Correctness for the WAM. TPHOLs
1996: 347-361
Tobias
Sean McLaughlin schrieb:
Email Gateway (Aug 18 2022 at 09:50):From: Alberto Momigliano <amomigl1@inf.ed.ac.uk>
You may also be interested in some (old) work by Mathieu Jaume
http://www-spi.lip6.fr/~jaume/
/A full formalisation of SLD resolution in the calculus of inductive
constructions <http://www-spi.lip6.fr/%7Ejaume/abstractjar.html>/,
Journal of Automated Reasoning, 23 (3-4):347-371,1999.
Best,
AM
Last updated: May 03 2024 at 12:27 UTC