Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle

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.

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

References in corpus (1)

• Complete Context Calculus Design and Implementation in GIPSY

Cited by in corpus (7)

• Intensional Cyberforensics
• Reasoning About a Simulated Printer Case Investigation with Forensic Lucid
• Cryptolysis v.0.0.1 - A Framework for Automated Cryptanalysis of Classical Ciphers
• Towards Improving Validation, Verification, Crash Investigations, and Event Reconstruction of Flight-Critical Systems with Self-Forensics
• Towards Automated Deduction in Blackmail Case Analysis with Forensic Lucid
• The Role of Self-Forensics in Vehicle Crash Investigations and Event Reconstruction
• Furthering Baseline Core Lucid Standard Specification in the Context of the History of Lucid, Intensional Programming, and Context-Aware Computing