Total Definitional Interpreters for Time and Space Complexity

Total Definitional Interpreters for Time and Space Complexity
Nils Anders Danielsson
Draft, 2018. [pdf, highlighted Agda code, zip file with code]

Abstract

Definitional interpreters are sometimes used to specify the semantics of programming languages and to reason about the semantics of programs. This text presents one way in which total definitional interpreters defined using the delay monad can be used to specify and reason about time and space complexity. The approach works for non-terminating programs, and the text is supported by machine-checked proofs.

Nils Anders Danielsson
Last updated Thu Oct 18 22:58:19 UTC 2018.