This looks really nice. Well done.
On Thu, Jul 25, 2013 at 5:01 PM, Vincent Aravantinos <
[email protected]> wrote:
> 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
>
>
------------------------------------------------------------------------------
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
