[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Invoking PVS Batch Mode in Haskell

To: pvs-help@xxxxxxxxxxx
Subject: [PVS-Help] Invoking PVS Batch Mode in Haskell
From: "J. Jaskolka" <jaskolj@xxxxxxxxxxxxxxxxxxxx>
Date: Thu, 03 Jul 2008 14:48:09 -0400
List-help: <mailto:pvs-help-request@csl.sri.com?subject=help>
List-id: PVS-Help <pvs-help.csl.sri.com>
List-post: <mailto:pvs-help@csl.sri.com>
List-subscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>
List-unsubscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hello,
 I am writing a Haskell program for which I would like to invoke PVS to
simplify some expressions and automate some proofs. I am curious to
know whether there is a way to invoke PVS batch mode in Haskell and if
so, how I might go about doing such a thing. Any help would be greatly
appreciated. Thanks for your time.

JJ

Prev by Date: RE: [PVS-Help] fullset type properties
Next by Date: Re: [PVS-Help] Unrecognized equality
Previous by thread: [PVS-Help] fullset type properties
Next by thread: [PVS-Help] some problems about list which is provided by the prelude
Index(es):
- Date
- Thread