Re: [isabelle] Rational numbers in Isabelle/ML

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.


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