DCS compared to termination checkers for type theories

Published: Sept. 19, 2023, 3 a.m.

b'

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

'