In that same vein, does anybody know anything about this effort? http://www.cs.cornell.edu/Info/Projects/NuPrl/
"The Nuprl proof development system is a framework for the development of formalized mathematical knowledge as well as for the synthesis, verification, and optimization of software. It is based on a significant extension of Martin-Lof's intuitionistic Type Theory [ML84]..." Downloadable here: http://www.cs.cornell.edu/Info/Projects/NuPrl/html/NuprlSystem.html Cheers, CY --- C Y <[EMAIL PROTECTED]> wrote: > Hey Tim. I recall some time back you mentioned some ideas you had > for > a "proper" redesign of Axiom, incorporating proof systems and some > fundamental design philosophy considerations, among other things. Is > there a summary of those thoughts somewhere? I'm having some trouble > finding it in the archives. > > Cheers, > CY > > > > ____________________________________________________ > Start your day with Yahoo! - make it your home page > http://www.yahoo.com/r/hs > > > > _______________________________________________ > Axiom-developer mailing list > Axiom-developer@nongnu.org > http://lists.nongnu.org/mailman/listinfo/axiom-developer > ____________________________________________________ Start your day with Yahoo! - make it your home page http://www.yahoo.com/r/hs _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
