Verified Programming of Turing Machines in Coq (2020)(popl20.sigplan.org)

popl20.sigplan.org

Verified Programming of Turing Machines in Coq (2020)

https://popl20.sigplan.org/details/CPP-2020-papers/6/Verified-Programming-of-Turing-Machines-in-Coq

1 comments

maxsun6 anni fa

I was recently reading into Total Functional Programming [1] and found it surprising that it seems possible to reason about/model Turing Machines in languages which guarantee a program's termination [2]. I've barely scratched the surface, but I feel like it's a fun combination of engineering and theoretical/philosophical issues. I'd super appreciate and fellow HNers suggestions for related resources or things to read.

[1] https://en.wikipedia.org/wiki/Total_functional_programming

[2] https://kseo.github.io/posts/2015-06-18-total-functional-pro...