[CakeML] Build problems
magnus.myreen at gmail.com
Thu Apr 6 11:14:02 UTC 2017
As far as I know, OpenTheory allows starting to record from a specific
point and allows the importer to map constants/types from one prover to
similar ones in the other system. -- Magnus
On Thu, 6 Apr 2017 at 12:14, Lars Hupel <hupel at in.tum.de> wrote:
> > What's your timeline for this project, and would you be interested in
> > working on producing an OpenTheory export of parts of CakeML with my
> > guidance?
> The timeline is "eventually" :-)
> But I'm not sure how well that would work in general. The major problem
> I foresee is this: You would replay definitions, including datatypes, in
> Isabelle, right? That means that those datatype definitions would mimic
> HOL's construction, and not Isabelle's construction. This likely means
> that I can't do anything useful with them.
> > Another approach would be to manually port the encoder/decoder
> > which might be more expedient but less satisfying and reusable.
> Not just more expedient but probably also faster. I'll take a stab.
> > They're not part of the semantics. There's overhead to using Lem, and
> > aren't formal guarantees that it produces the same semantics in multiple
> > systems (although I believe a fair amount of work has gone into ensuring
> > that is usually the case).
> Fair enough.
> Thanks for all the help so far!
> Users mailing list
> Users at cakeml.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Users