Hi list,
I recently gave a tutorial about HOL internals here in Concordia and I
though it might be useful to share with the community, in case anyone is
interested.
Objective of the tutorial: provide a deeper idea of how HOL works.
Intended audience: people having some experience of HOL as users and
wanting to know more about how HOL works "from inside", but who do not
necessarilly have much background in logic nor functionnal programming.
To do so we develop a simplistic theorem prover for *propositional* logic:
it is of course useless to do actual mathematics but enables to understand
the fact that terms are Ocaml/SML values, how we use abstract datatypes to
represent theorems and how the tactic system works.
The prover is called "ZOL" for Zero-Order Logic. The sources are less than
200 lines and are available both in Ocaml and SML.
Slides: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.pdf
Ocaml source: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.ml
SML source: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.sml
Main page: http://users.encs.concordia.ca/~vincent/Teaching.html
Regards,
V.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
See everything from the browser to the database with AppDynamics
Get end-to-end visibility with application monitoring from AppDynamics
Isolate bottlenecks and diagnose root cause in seconds.
Start your free trial of AppDynamics Pro today!
http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
