[Axiom-developer] Verified Computer Algebra in ACL2

2015-07-10 Thread daly
I'm Tim Daly, Lead developer on the Axiom computer algebra system. I'm reading the paper Verified Computer Algebra in ACL2. Is the code available somewhere? I'd like to reproduce the result and understand the details. Tim Daly http://daly.axiom-developer.org

[Axiom-developer] Proving Axiom correct

2015-07-10 Thread daly
There is a free book Certified Programming with Dependent Types about COQ available at: http://adam.chlipala.net/cpdt/cpdt.pdf Tim ___ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer

Re: [Axiom-developer] Literate programming

2015-07-10 Thread daly
William, Back in the day I struggled to cross the great chasm, moving from real programming to structured programming, i.e. not using GOTOs. Dijkstra was asking me to change a fundamental part of my thinking, to throw away the focus on the machine's BRANCH instruction, albeit in my high-level