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: Sep 25 2021 at 08:21 UTC