Coq certified relative Hilbert-Post completeness proofs for states and exceptions (core and programmers' languages) effects when formalized in decorated logics. This briefly tells us that if an algebraic theory is extended with states and/or exceptions effects in the given way, then its completeness will not get any worsened: it will remain Hilbert-Post complete if it has already been.
ekiciburak / hpc Goto Github PK
View Code? Open in Web Editor NEWRelative Hilbert-Post completeness for states and exceptions (core and programmers' languages) effects when formalized in decorated logics.
Home Page: http://coqeffects.forge.imag.fr/
License: Other