Re: [isabelle] Rational numbers in Isabelle/ML

> On 2 Apr 2016, at 10:58 PM, Makarius <makarius at> wrote:
> On Sat, 2 Apr 2016, Lawrence Paulson wrote:
>> CakeML illustrates the advantages of a formal definition. It is a subset of standard ML with substantially the same semantics. Without a formal semantics, the very idea of a verified compiler is meaningless. Others have also noticed the benefits of using a formally defined language for coding a theorem prover.
> It would be great to see a fully verified CakeML compiler + runtime system
> + proof checker, and Isabelle export to that for independent checking.
> As a start, someone could put the old Isabelle/OpenTheory implementation by Brian Huffman into shape.

We (Sydney team, including Ramana and Michael on the HOL4 side) are interested in working on that in the medium term, i.e. in a few months to a year or so.

If anyone else is interested as well, let us know, more than happy to collaborate on it!



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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