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