Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle

Simple item page
dc.creatorMokhov, Serguei A.
dc.creatorPaquet, Joey
dc.date2009-04-24
dc.date.accessioned2026-07-07T13:12:33Z
dc.date.available2026-07-07T13:12:33Z
dc.descriptionA 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.
dc.description23 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
dc.identifierhttps://arxiv.org/abs/0904.3789
dc.identifierhttp://arxiv.org/abs/0904.3789
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/229611
dc.subjectLogic in Computer Science
dc.subjectCryptography and Security
dc.subjectProgramming Languages
dc.subjectD.3.1; D.3.2; D.3.3; D.3.4
dc.titleFormally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle
dc.typetext

Files

Collections

arXiv