[isabelle-dev] support for ideas using isabelle hol

[David Blubaugh]

Hello,
 
 
My name is DAvid Blubaugh.
 
 
I want to state that I am in the process of using advanced machine learning techniques to use Isabelle HOL to inspect and develop quality assurance for software applications 1!!
 
I was wondering if there are any sources of support out there might be interested in such technologies???  
 
thanks,
 
 
David
 
 
 


________________________________
From: "isabelle-dev-request at mailbroy.informatik.tu-muenchen.de" <isabelle-dev-request at mailbroy.informatik.tu-muenchen.de>
To: isabelle-dev at mailbroy.informatik.tu-muenchen.de 
Sent: Sunday, August 25, 2013 6:00 AM
Subject: isabelle-dev Digest, Vol 75, Issue 31


Send isabelle-dev mailing list submissions to
    isabelle-dev at mailbroy.informatik.tu-muenchen.de

To subscribe or unsubscribe via the World Wide Web, visit
    https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

or, via email, send a message with subject or body 'help' to
    isabelle-dev-request at mailbroy.informatik.tu-muenchen.de

You can reach the person managing the list at
    isabelle-dev-owner at mailbroy.informatik.tu-muenchen.de

When replying, please edit your Subject line so it is more specific
than "Re: Contents of isabelle-dev digest..."


Today's Topics:

  1. Re: functions over abstract data (Alexander Krauss)
  2. Re: The coming release (Alexander Krauss)


----------------------------------------------------------------------

Message: 1
Date: Sat, 24 Aug 2013 23:20:19 +0200
From: Alexander Krauss <krauss at in.tum.de>
To: Christian Sternagel <c.sternagel at gmail.com>
Cc: isabelle-dev <isabelle-dev at mailbroy.informatik.tu-muenchen.de>
Subject: Re: [isabelle-dev] functions over abstract data
Message-ID: <52192393.9080503 at in.tum.de>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

Hi Chris,

[...]

> When defining a function "f", whose result type is "T", it might be
> necessary to "peek under the hood" in order to show termination. When
> doing this manually, we destroy the abstraction and always have to
> reason about the raw-level and even worse, also all the existing
> constants with result type T have to be deconstructed in the definition.

I discussed similar ideas with John Matthews around 2007/8, where we 
also had a recursive specification of a value that could "internally" be 
expressed as a recursive function, even though it was not of function 
type itself. The (single) motivation at the time was the attempt to 
define infinite streams, modelled basically as "nat => 'a". However, I 
abandoned the approach as too complicated. For streams, I believe they 
should be more naturally defined corecursively. The same might hold for 
your parsers if you find a good way of expressing it: Your "par" 
definition is well-formed because the recursive call is wrapped into 
something else... This looks more like a productivity argument then a 
termination one, even though, when unfolding, one can be seen as the other.

Do you know the work of Nils Anders Danielsson on parsers, in particular
http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf
?
I'm not sure what this would mean in HOL, but it is certainly relevant.


[...]
> Here comes my suggestion
[...]

What you are proposing would add substantial complexity to pretty much 
everything in the function package. While it might be possible to do 
such a thing ("no obvious deficiencies"), you would pay later when 
maintaining the stuff. This is too much for what seems to me like a 
"one-man-feature".


> PS: I started to dive into the function package. My first hurdle is that
> for "f" not of function type (as in "par"), no recursive calls are
> generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules
> could be found".

The analysis in the function package assumes basically a form where the 
arguments of recursive calls can be extracted explicitly. This is a hard 
assumption, and I see no chance of getting rid of it. The only sensible 
way of lifting this restriction is to build some sort of wrapper that 
reduces some other format to a normal function definition.

Alex



------------------------------

Message: 2
Date: Sat, 24 Aug 2013 23:27:33 +0200
From: Alexander Krauss <krauss at in.tum.de>
To: Makarius <makarius at sketis.net>
Cc: isabelle-dev at in.tum.de
Subject: Re: [isabelle-dev] The coming release
Message-ID: <52192545.1030305 at in.tum.de>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

On 08/17/2013 04:05 PM, Makarius wrote:
> in the past few weeks the coming release has been mentioned in passing
> several times.  So far the precise schedule is not clear, but just from
> the distance to Isabelle2013 and the amount of material that is about to
> be finished for Isabelle2013-1, it has to be rather soon after the summer.
>
> Since Isabelle is a huge and complex system, things that are relevant
> for a release need to be known well in advance.

There is a small extension to the function package pending, which was 
written by Manuel Eberl. It produces elimination rules of a new format, 
and also provides a "fun_cases" command for ad-hoc elimination that is 
analogous to "inductive_cases".

Since there is some user demand for it and it is already functionally 
complete, I'd like to integrate this when I am back from vacation in two 
weeks, even if there are some minor things to be sorted out.

Alex




------------------------------

Subject: Digest Footer

_______________________________________________
isabelle-dev mailing list
isabelle-dev at mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


------------------------------

End of isabelle-dev Digest, Vol 75, Issue 31
********************************************
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130825/56acc58d/attachment.html>