—Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This al...
Dmitriy Traytel, Andrei Popescu, Jasmin Christian ...
I describe the mechanisation in HOL of some basic -calculus theory, using the axioms proposed by Gordon and Melham [4]. Using these as a foundation, I mechanised the proofs from C...