What Codata, Control Flow, and Logic Teach Us About Programming

This article breaks down the λμμ̃-calculus using simple examples to explain key ideas in logic, control flow, and how programs run. It's a helpful guide for anyone curious about how programming languages work under the hood.

Table of Links

A. The Relationship to the Sequent Calculus

B. Typing Rules for Fun

C. Operational Semantics of label/goto

References

6 Related Work

The central ideas of the calculi that we have presented in this pearl are not novel: the 𝜆𝜇𝜇˜-calculus is by now over 20 years old. We chose a variant of this calculus that can be used as a starting point to explore all the variants that have been described in the literature. This related work section is therefore intended to provide suggestions for further reading and the chance to dive deeper into specific topics that we have only touched upon.

6 ...