I've been looking at integrating formal methods, advanced typing and provability into STEPS, mainly as a good solution to being able to go from specifications to testable prototypes easily. I've been looking at a number of different languages and proof assistants that could fill the role. >From the (little) reading I've done, there seems to be a concensus that higher order languages/provers are more useful than first order ones, in particular, pattern matching for types/solutions appears to be more complete under higher order logic. For example, Epigram http://www.e-pig.org/darcs/Pig09/web/ is based on dependent types, but uses first order matching and is incomplete (see the literal programming manual, Epitome, p163) ie. it doesn't neccessarily match all types/terms. I'm of the opinion that, although having a sound and complete parser/matcher is pretty useless day-to-day (most computer languages and systems are unambiguous), it is important to be sure you'll catch all types/terms for proofs and for execution.
Coq, Isabelle and PVS all now use rewriting to some extent, though in a higher order fashion (ie. more general than lambda calculus eg. Curry-Howard calculi, dependent types). They do appear to use first-order logic for some proofs where decidability is a problem ( www.lix.polytechnique.fr/~jouannaud/articles/tyl.pdf) and having seen some higher-order developments within Maude, I'd venture that it is useful to build higher-order provers on first-order environments - case in point, Epigram compiles down to Haskell constructs. There's a very good paper on pure type systems in Maude, with a view to implementing a higher-order (Open) Calculus of Constructions. The paper mentions a nice CINNI notation which allows you to use named types, rather than say de Brujin indices, and still avoid accidental type/term hiding. The proof assistant for OCC has been designed for use in a universe heirarchy ( http://www.informatik.uni-hamburg.de/TGI/mitarbeiter/wimis/stehr/occ_eng.html) which does sound similar to Alessandro Warth's Worlds POV. A later paper on the system is here: http://www.arnetminer.org/viewpub.do?pid=882439 It looks interesting, but I don't have a direct link for download unfortunately. Lastly, I've a couple of links to a declarative debugger in Maude - yes you can debug the specifications! (http://maude.sip.ucm.es/debugging/ and http://maude.cs.uiuc.edu/papers/pdf/Riesco-et-al-debugging-tr.pdf) Fairly recently, the Maude team (and contributors) wrote a formal analyser for java programs (JavaFAN - see the slides in the Maude intro http://maude.cs.uiuc.edu/talks/maude-padl10-slides.pdf). The basic strategy I've come up with, involves writing a version of Maude on top of Squeak (smalltalk), then adapting JavaFAN to analyse smalltalk bytecodes so you can prove the version of Maude itself, the VM, and thus the entire software stack from the top, down to the metal by virtue of running on the VM (ok, SqueakNOS isn't strictly bare metal, but STEPS/FRANK/NotSqueak should be, and I'd try to move the Maude runtime across). The Maude port would be straight - I don't know smalltalk that well, and I'm starting work by moving over the BuDDY library into Squeak. I'd appreciate people's thoughts on my programming direction. Cheers, Alexis.
_______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
