Hi, I want to formalize first-order logic on graphs (see https://doi.org/10.4204/EPTCS.330.11 ;Section 3) using a deep embedding. I started reading "Concrete Semantics" by Nipkow and Klein followed by "Certifying Machine Code Safety: Shallow versus Deep Embedding" by Wildmoser and Nipkow and recently found a techn. report by Volker "A Deep Embedding of ZC in Isabelle/HOL" (http://repository.essex.ac.uk/14449/) in which De Bruijn terms are used. Based on my limited understanding, this approach makes much sense to represent my logic, so-far . Any thoughts\guidance\comments would be highly appreciated.
Last updated: Aug 13 2022 at 05:18 UTC