Abstraction in Programming Language Theory - Howe's Method

Explore a research colloquium presentation that delves into the abstraction of programming language theory, specifically focusing on Howe's method for proving applicative bisimilarity. Learn how category theory can be applied to establish an abstract congruence theorem that unifies various adaptations of Howe's method across different programming languages. Discover how this theoretical framework bridges the gap between language-specific implementations, from call-by-name and call-by-value λ-calculus to PCF, λ-calculus with delimited continuations, and higher-order π-calculus. Understand the significance of creating a unified approach to program equivalence proofs, moving beyond the traditional language-by-language research methodology in programming language theory. Based on joint research work, this presentation demonstrates how mathematical abstraction can elegantly capture and generalize key concepts across multiple programming language paradigms.