>> -- 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 ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/T5e30c339c3bfa713-M4aa6a12057d95e05ba103c9e Delivery options: https://agi.topicbox.com/groups/agi/subscription
