Input/output logic; Isabelle/HOL; General Data Protection Regulation
Résumé :
[en] 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.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
FARJAMI, Ali ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
MEDER, Paul Joseph Yves ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC)
PARENT, Xavier ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
BENZMÜLLER, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
I/O Logic in HOL
Date de publication/diffusion :
17 septembre 2018
Nom de la manifestation :
MIREL 2018 workshop on MIning and REasoning with Legal texts
Organisateur de la manifestation :
University of Luxembourg
Lieu de la manifestation :
Luxembourg
Date de la manifestation :
17-09-2018
Manifestation à portée :
International
Projet européen :
H2020 - 690974 - MIREL - MIREL - MIning and REasoning with Legal texts