I/O Logic in HOL
Christoph Benzmüller, Ali Farjami, Paul Joseph Yves Meder, Xavier Parent – 2018
A shallow semantical embedding of Input/Output logic in classical higher-order logic is presented, and shown to be faithful (sound an complete). This embedding has been implemented in the higher-order proof assistant Isabelle/HOL. We provide an empirical regulative framework for assessing General Data Protection Regulation.