Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa
Department of Mathematics, Computer Science and Physics - University of Udine, Italy - May 2019

Web Appendix of the paper: "A definitional implementation of the Lax Logical Framework LLFP in Coq,
for supporting fast and loose reasoning", accepted for publication at LFMTP 2019 (Vancouver, Canada)
- file LLFP: implementation of LLFP in the Coq proof assistant version 8.8.2
- file lambda: call-by-value lambda-calculus (case study 1)
- file branch: branch-prediction for URM machines (case study 2)