Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle
Logic in Computer Science
2009-05-08 v1 Cryptography and Security
Programming Languages
Abstract
A Forensic Lucid intensional programming language has been proposed for intensional cyberforensic analysis. In large part, the language is based on various predecessor and codecessor Lucid dialects bound by the higher-order intensional logic (HOIL) that is behind them. This work formally specifies the operational aspects of the Forensic Lucid language and compiles a theory of its constructs using Isabelle, a proof assistant system.
Keywords
Cite
@article{arxiv.0904.3789,
title = {Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle},
author = {Serguei A. Mokhov and Joey Paquet},
journal= {arXiv preprint arXiv:0904.3789},
year = {2009}
}
Comments
23 pages, 3 listings, 3 figures, 1 table, 1 Appendix with theorems, pp. 76--98. TPHOLs 2008 Emerging Trends Proceedings, August 18-21, Montreal, Canada. Editors: Otmane Ait Mohamed and Cesar Munoz and Sofiene Tahar. The individual paper's PDF is at http://users.encs.concordia.ca/~tphols08/TPHOLs2008/ET/76-98.pdf