Did you happen to read the posts I wrote on using Xavier LeRoy's certified compiler building methodology to create a "object-oriented browser" that doesn't succumb to Dan Ingalls' Smalltalk "live image" problem?
On Fri, Jul 15, 2011 at 5:36 PM, Alexis Read <[email protected]> wrote: > 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<http://www.lix.polytechnique.fr/%7Ejouannaud/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 >
_______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
