The Delta-calculus: syntax and types

Luigi Liquori, Claude Stolze

We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different inter…