[isabelle-dev] support for ideas using isabelle hol

Sun Aug 25 23:19:57 CEST 2013

The main avenue for support is the users' mailing list, which is isabelle-users at cl.cam.ac.uk. You have mailed the developers' list.

I do suggest that you frame your question to include more technical detail, because as things stand it's impossible to imagine what you are trying to do.

Larry Paulson

On 25 Aug 2013, at 20:22, David Blubaugh <davidblubaugh2000 at yahoo.com> wrote:

> 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
> ********************************************
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130825/66e48f3e/attachment-0002.html>