> Indeed. What would be such classical papers from your field? One paper I have in mind is Hodgkin & Huxley's paper published in 1952 where they first wrote down the equations describing the membrane voltage of the giant squid axon. https://www.ncbi.nlm.nih.gov/pmc/articles/PMC1392413/pdf/jphysiol01442-0106.pdf
It'll be a good exercise for me to go through it and write a summary, transcribing the equations into the Leibniz notation. > I have vaguely played with that idea myself, but I don't know the > capabilities of today's proof assistants well enough to judge how they > could be used in the evaluation of scientific models. Do you have > a concrete application in mind? Something that could be done today > if the learning-curve issue could be overcome? Currently I only have a limited exposure to proof assistants, so I hesitate to say anything definitive. I'm focusing on Isabelle right now at tutorial stage since I heard from various sources that HOL-type assistants are more useful for real analysis problems. Isabelle belongs to that category which is the reason I'm looking at it more closely. No firm concrete applications in mind, it's an open-ended exploration. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
