Plug and Play the Theory of Contexts in Higher-Order Abstract Syntax
Alberto Ciaffaglione, Ivan Scagnetto · Electronic Notes in Theoretical Computer Science · 2004
We illustrate the pragmatic aspects of the Theory of Contexts, recently proposed as a general approach for reasoning on languages with binders in Higher-Order Abstract Syntax, through two working examples: λ-calculus and Abadi and Cardelli’s impς-calculus.