Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle
Serguei A. Mokhov, Joey Paquet · Spectrum Research Repository (Concordia University) · 2009
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.