>> -- design of a new programming language (MeTTA = Meta Type Talk) >> designed to serve as the type system and formalism behind the new >> version of OpenCog Atomspace. A lot of math/CS work has been done in >> the last 9 months leading up to this design... > > > Meta Type Talk... > > Is it a fair guess that there will be an element of Category Theory, sheaves, > and the like, in MTT? >
MeTTA has def. been designed with the triad of (programming languages, categories, logics) in mind... Working out the specifics of the Curry-Howard mapping from MeTTa to intuitionistic logics, and from there to categorial semantics, is one of the things on our plate for the next couple months This will then allow a more rigorous and MeTTA-flavored version of the stuff I sketched out here https://arxiv.org/abs/2012.14474 as well as formulation of e.g. stuff from modal HoTT in MeTTA terms https://golem.ph.utexas.edu/category/2020/02/modal_homotopy_type_theory_the.html ben -- You received this message because you are subscribed to the Google Groups "opencog" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CACYTDBf4yXcpuZXETARr0o8xz3vuMSa0KTsSsfm2bDRBGEaZnA%40mail.gmail.com.
