This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other fo...
eXtensible Business Reporting Language (XBRL) presents new opportunities for integrating information flow within communities of diverse organisations thereby significantly enhanci...
mentation of the Abstraction Method In Coq Eelis van der Weegen Institute for Computing and Information Sciences Raboud University Nijmegen This technical report documents our deve...
Herman Geuvers, Adam Koprowski, Dan Synek, Eelis v...
rder Abstract Syntax in Isabelle/HOL Douglas J. Howe Carleton University July 13, 2010 Douglas J. Howe (Carleton University) HOAS in Isabelle/HOL July 13, 2010 1 / 8
Influenced by the success of the MIZAR system many declarative proof languages have been developed in the theorem prover community, as declarative proofs are more readable, easier...