Talking About Computation

Well, I can talk about it, but I don't class this as thinking really.


See Magma (algebra) for a definition of groupoids.

See Magma - Computer Algebra System and https://prooftoys.org/ian-grant/hm/. And I have just learned something really interesting about prooftoys from a github repo where it is said that the proof assistant is based on an implementation (called Q0) of Church's Simple Theory of Types by Professor Peter Andrews (CMU Emeretus). You can read about the ETPS (Educational Theorem Proving System) in ETPS: A System to Help Students Write Formal Proofs.

Comments

Popular posts from this blog

Live Science - Leonardo da Vinci's Ancestry

David Turner Obituary by Sarah Nicholas Fri 24 Nov 2023