Re: [isabelle] Where to learn about HOL vs FOL?



On Wed, 06 Feb 2013 16:19:03 +0100, Makarius <makarius at sketis.net> wrote:
People seems to care, only when they have to port some proof from one
system to another. There seems to be multiple HOL4 to Isabelle papers on
the web, and seems all are concerned with foundations.

These converters usually try to convert the "object-code".  There are
interesting ongoing projects like
https://www.rocq.inria.fr/deducteam/Dedukti/ with potentially interesting
applications of moving huge lambda terms back and forth between systems.

The high-level problem of moving huge applications from prover X to prover Y is not addressed at all.

Isn't it what OpenTheory is for? Or I may have not understand what it is; will get time to have a real look at it later.

--
Yannick Duchêne





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.