[Hol-info] CakeML postdoc opportunity

a new benchmark for building refactoring tools for programming languages in general. The project, which is coordinated by Prof Simon Thompson and Dr Scott Owens, will support two research associates, and the four will work as a team. One post will focus on pushing the boundaries of trustworthy

Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

und 2013, new_specification has been extended >> to relax >> certain constraints on polymorphism that it imposed. The resulting >> gen_new_specification >> has been proved conservative informally by me and formally in HOL4

[Hol-info] Proving a trivial goal

Does anyone know how to prove this goal: ∀(p1,p1',p2). T I’m not sure how I got it, and I can’t work out how to prove it, but it’s probably true :) Scott -- ___ hol-info

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Among others, LENGTH (FILTER (\e. X = e)) = 1 Scott > On 2017/10/05, at 15:55, Chun Tian (binghe) wrote: > > But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just > the appearance of certain element is only one. —Chun > >> Il giorno 05 ott 2017,

[Hol-info] PhD studentship on the CakeML project (University of Kent)

must have, or be about to complete a degree in Computer Science or Mathematics at the BSc or MSc level. The position is fully funded for 3.5 years for students from the UK/EU. Interested candidates should contact me by 21 May, 2018. Scott Owens http://www.cs.kent.

Re: [Hol-info] hardware verification and dependent types

This doesn’t directly answer the question, but the Sail project (https://www.cl.cam.ac.uk/~pes20/sail/) designed a relatively lightweight dependent type mechanism for describing ISAs. Scott > On 2019/04/30, at 14:28, Lawrence Paulson wrote: > > In hardware, most devices are parameterised by