Input/output logic; Isabelle/HOL; General Data Protection Regulation
Abstract :
[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 :
Computer science
Author, co-author :
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)
External co-authors :
yes
Language :
English
Title :
I/O Logic in HOL
Publication date :
17 September 2018
Event name :
MIREL 2018 workshop on MIning and REasoning with Legal texts
Event organizer :
University of Luxembourg
Event place :
Luxembourg
Event date :
17-09-2018
Audience :
International
European Projects :
H2020 - 690974 - MIREL - MIREL - MIning and REasoning with Legal texts
