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

[Scott Owens]

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 a numerical bit width: buses, 
> counters, adders, registers, etc. So it seems obvious that people might have 
> tried to perform hardware verification using some form of dependent type 
> theory. Are there any particularly notable achievements along those lines? 
> And if not, why not?
> 
> Larry Paulson
> 
> 
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Scott Owens]

I am looking for a PhD student to work with me on the CakeML project at the
University of Kent in Canterbury, England. The position is part of the
"Building Verified Applications in CakeML" project funded by the UK Research
Institute in Verified Trustworthy Software Systems:
https://vetss.org.uk/funded-proposals/.

CakeML (https://cakeml.org) is a formally verified compiler for an ML-like
programming language. The studentship is focussed on techniques for formally
verifying applications written in the CakeML language. Within the project,
there is a wide range of possible topics, ranging from fully automated
verification to techniques requiring interactive proof, and also from the logic
and mathematics that underpin verification to the creation of a practical
verification tool chain.

The student will be studying in the University of Kent's programming languages
research group which has 13 faculty members, and has notable strengths in
verification, concurrency, and functional programming. He or she will also work
with the broader international CakeML community at Chalmers (Sweden), CMU
(USA), and Data61 (Australia).

The position starts in September 2018. Applicants 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.ac.uk/~sao


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Scott Owens]

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, alle ore 16:48, Konrad Slind  
>> ha scritto:
>> 
>> Hi Chun Tian,
>> 
>>  The constant ALL_DISTINCT in listTheory is what you are looking for, I 
>> think.
>> 
>> Konrad.
>> 
>> 
>> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe)  
>> wrote:
>> Hi,
>> 
>> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
>> possibly duplicated elements, and I want to express certain element X is 
>> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
>> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
>> 
>> Regards,
>> 
>> Chun Tian
>> 
>> --
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>> 
>> 
>> --
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> 
>> 
> 
> --
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! 
> http://sdm.link/slashdot___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Proving a trivial goal

[Scott Owens]

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 mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Scott Owens]

I don’t want to put words in Rob’s mouth, as he’s far more knowledgable in this 
area than I am.

As far as I know, there is no mechanised conservativity proof for HOL’s recent 
generalised constant specification mechanism. (Here I’m in agreement that 
“conservativity” without any other modification should refer to the proof 
theoretic notion, and that’s what I mean here.) Rob certainly has a 
pencil-and-paper proof. Ramana, Rob, Magnus, and I (although mostly Ramana) 
proved the soundness of a HOL Light-style logical system, including the 
generalised constant specification mechanism that Rob refers to (and also 
designed) and type definition mechanism, with respect to a standard model of 
higher-order logic. I worked on a mechanised conservativity proof for the 
definition mechanism for a bit two years ago but got distracted and haven’t 
returned to it. I think it would be a suitable student project, but I’m not 
convinced that it’s really that interesting — I wouldn’t be bothered by a sound 
and consistent definition principle that allowed one to prove more things.

Scott


> On 2016/10/22, at 20:07, Ondřej Kunčar <kun...@in.tum.de> wrote:
> 
> Hi Rob,
> you are right that we mention only the plain definitions in HOL and not 
> the implicit ones, when we compare the definitional mechanism of HOL and 
> Isabelle/HOL. (If this what you meant; I assume you didn't mean to say 
> that the overloading in Isabelle is 25 years out of date).
> I clearly remember that one of the early versions of our paper contained 
> the comment that the current HOL provers use the more powerful mechanism 
> that you mentioned but I guess that it was lost during later editing. We 
> will include it again into the journal version of the paper.
> 
> I wanted to comment on your statement that A. Pitts proved that 
> definitions in HOL are conservative. Such statements are always a little 
> bit puzzling to me because when you say conservative (without any 
> modifier), I always think that you mean the notion that "nothing new can 
> be proved if you extend your theory (by a definition)". I think a lot of 
> people (including me) think that this is THE conservativity. There is 
> also a notion of the model-theoretic conservativity that requires that 
> every model of the old theory can be expanded to a model of the new 
> theory. This is a stronger notion and implies the proof conservativity.
> 
> As far as I know, A. Pitts considers only a subset of all possible 
> models (so called standard models) in his proof and he only proves that 
> these models can be extended from the old to the new theory. But as far 
> as I know this does not imply the proof conservativity.
> 
> Best,
> Ondrej
> 
> On 10/22/2016 12:59 PM, Rob Arthan wrote:
>> Ken,
>> 
>> Unfortunately, the paper by Ondrej Kuncar and Andrei Popescu that you cite 
>> gives
>> a description of the definitional mechanisms in HOL that is about 25 years 
>> out of date.
>> The new_specification mechanism allows implicit definitions and cannot be 
>> viewed
>> as a syntactic abbreviation mechanism. There is a proof of the 
>> conservativeness of a
>> (generalisation of) this mechanism in Andy Pitts’ Introduction to the HOL 
>> Logic (ref. [31]
>> in the paper). new_specification is implemented in all the "HOL-based 
>> provers” listed
>> in the paper.
>> 
>> Due to tinkering on my part around 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 by Ramana 
>> Kumar,
>> Magnus Myreen and Scott Owens  (see their and my papers in ITP 2014 and/or 
>> JAR 56(3)).
>> gen_new_specification is implemented (to my knowledge) in HOL4, ProofPower 
>> and OpenTheory.
>> 
>> Regards,
>> 
>> Rob.
>> 
>> 
> 
> 
> --
> Check out the vibrant tech community on one of the world's most 
> engaging tech sites, SlashDot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
Check out the vibrant tech community on one of the world's most 
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] CakeML postdoc opportunity

[Scott Owens]

I’m presently looking (with Simon Thompson) for two Post Docs to work on a 
CakeML and HOL related project. The posts last for 3.5 years and are at the 
University of Kent in Canterbury, England. Applications are due by *12 June, 
2016*.

Here is a brief description of the project:

Trustworthy Refactoring project: Research Associate Positions in Refactoring 
Functional Programs and Formal Verification (for CakeML) 

The Trustworthy Refactoring project at the University of Kent is seeking to 
recruit postdoc research associates for two 3.5 year positions, to start in 
September this year.

The overall goal of this project is to make a step change in the practice of 
refactoring by designing and constructing of trustworthy refactoring tools. By 
this we mean that when refactorings are performed, the tools will provide 
strong evidence that the refactoring has not changed the behaviour of the code, 
built on a solid theoretical understanding of the semantics of the language. 
Our approach will provide different levels of assurance from the (strongest) 
case of a fully formal proof that a refactoring can be trusted to work on all 
programs, given some pre-conditions, to other, more generally applicable 
guarantees, that a refactoring applied to a particular program does not change 
the behaviour of that program. 

The project will make both theoretical and practical advances. We will build a 
fully-verified refactoring tool for a relatively simple, but full featured 
programming language (CakeML https://cakeml.org), and at the other we will 
build an industrial-strength refactoring tool for a related 
industrially-relevant language (OCaml). This OCaml tool will allow us to 
explore a range of verification techniques, both fully and partially automated, 
and will set 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 refactoring via 
mechanised proof for refactorings in CakeML, and the other post will 
concentrate on building an industrial strength refactoring tool for OCaml. The 
project has industrial support from Jane Street Capital, who will contribute 
not only ideas to the project but also host the second RA for a period working 
in their London office, understanding the OCaml infrastructure and their 
refactoring requirements.

You are encouraged to contact either of the project investigators by email 
(s.a.ow...@kent.ac.uk, s.j.thomp...@kent.ac.uk) if you have any further 
questions about the post, or if you would like a copy of the full research 
application for the project. We expect that applicants will have PhD degree in 
computer science (or a related discipline) or be close to completing one. For 
both posts we expect that applicants will have experience of writing functional 
programs, and for the verification post we also expect experience of developing 
(informal) proofs in a mathematical or programming context.

To apply, please go to the following web pages:

Research Associate in Formal Verification for CakeML (STM0682): 

https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=4A515F4E5A565B1A=40106,3472764668=47167934=549534472123=sejmwzlocjpwfyyfak

Research Associate in Refactoring Functional Programs (STM0683): 

https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=4A515F4E5A565B1A=40107,6987525698=47167934=549534472123=sesioeandjktfucacs

Simon and Scott
--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info