DCS compared to termination checkers for type theories

Iowa Type Theory Commute

Aaron Stump द्वारा प्रदान की गई सामग्री. एपिसोड, ग्राफिक्स और पॉडकास्ट विवरण सहित सभी पॉडकास्ट सामग्री Aaron Stump या उनके पॉडकास्ट प्लेटफ़ॉर्म पार्टनर द्वारा सीधे अपलोड और प्रदान की जाती है। यदि आपको लगता है कि कोई आपकी अनुमति के बिना आपके कॉपीराइट किए गए कार्य का उपयोग कर रहा है, तो आप यहां बताई गई प्रक्रिया का पालन कर सकते हैं https://hi.player.fm/legal।

1y ago 19:45

MP3•एपिसोड होम

In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here.

166 एपिसोडस

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille