Induction on Concurrent Terms
Anders Schack-Nielsen · Electronic Notes in Theoretical Computer Science · 2008
This paper considers MiniML equipped with a standard big-step semantics and a destination-passing semantics both represented in concurrent LF (CLF) and prove the two semantics equivalent. The proof is then examined yielding insights into the issues concerning induction on concurrent terms. We conclude by outlining some of the difficulties that one will need to address when designing a meta-logic for CLF.