<p>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 <a href='https://gitlab.com/astump97/dcs'>here</a>. </p>

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.

<p>In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean.&nbsp; I warmly invite ITTC listeners to experiment with the tool themselves.&nbsp; The repo is <a href="https://gitlab.com/astump97/dcs" rel="noopener noreferrer">here</a>.&nbsp;</p>

DCS compared to termination checkers for type theories

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share DCS compared to termination checkers for type theories

Sign up to save your podcasts

DCS compared to termination checkers for type theories

DCS compared to termination checkers for type theories