Dear HOL users
Would anyone be interested in entering a team using HOL4 or HOL Light to
the Verified Software: Theories, Tools and Experiments competition next
year (2013)?
Information about the last competition is here:
https://sites.google.com/site/vstte2012/.
Winning teams used ACL2, KIV,
On Wed, Jun 6, 2012 at 1:51 PM, Rob Arthan r...@lemma-one.com wrote:
Tom Ridge and I formed two teams of one each using HOL4 and ProofPower-HOL
(respectively) in the first VSTTE competition which was a slightly smaller
scale affair at the previous VSTTE (it was a rather open-ended 2 hours
On Wed, Jun 6, 2012 at 6:33 PM, Ramana Kumar ramana.ku...@gmail.com wrote:
Cv1_Axiom;
val it =
|- ∀f0 f1 f2 f3 f4 f5 f6 f7.
∃fn0 fn1 fn2.
(∀l. fn0 (CLitv l) = f0 l) ∧
(∀m vs. fn0 (CConv m vs) = f1 m vs (fn1 vs)) ∧
(∀env xs b. fn0 (CClosure env xs b) = f2 env
On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind konrad.sl...@gmail.com wrote:
Note that Datatype.build_tyinfos is only guaranteed to work on
types that Hol_datatype produces. Does your datatype have
some other features?
Yes, recursion through the range of a finite map.
It wasn't _too_
Sounds like a bug. Can you send me sources?
Thanks,
Konrad.
On Wed, Jun 6, 2012 at 1:30 PM, Ramana Kumar ramana.ku...@gmail.com wrote:
On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind konrad.sl...@gmail.com wrote:
Note that Datatype.build_tyinfos is only guaranteed to work on
types that
Tom Ridge and I formed two teams of one each using HOL4 and ProofPower-HOL
(respectively) in the first VSTTE competition which was a slightly smaller
scale affair at the previous VSTTE (it was a rather open-ended 2 hours during
the conference rather than 48 hours strictly timed several weeks
