A modification of simply-typed λ-calculus by generalized elimination rules in the style of von Plato is presented. Its characteristic feature are permutative conversions also for function types and product types. After the addition of certain extensional reduction rules, and interpolation theorem (a la Lyndon) is proven which is also aware of the terms (a. k. a. the proofs via the Curry-Howard-isomorphism) like in Cubric's treatment of the usual λ-calculus. Connections between interpolation and canonical liftings of positive and negative type dependencies are given which are important for the intensional treatment of inductive datatypes.
展开▼
