scientific article; zbMATH DE number 512797
From MaRDI portal
Publication:4281490
zbMath0786.03006MaRDI QIDQ4281490
Publication date: 7 April 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Church-Rosserdivide-and-conquer lemmaMints' reduction for ccc-calculusrestricted \(\eta\)-expansionrestricted \(\pi\)-expansionStrong Normalization
Related Items (18)
Syntactic analysis of \(\eta\)-expansions in pure type systems. ⋮ Some lambda calculi with categorical sums and products ⋮ Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ On the power of simple diagrams ⋮ Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type ⋮ Higher-order families ⋮ Combining algebraic rewriting, extensional lambda calculi, and fixpoints ⋮ On the semantics of the universal quantifier ⋮ On modular properties of higher order extensional lambda calculi ⋮ Embedding of a free cartesian-closed category into the category of sets ⋮ Developing developments ⋮ A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object ⋮ Combining first order algebraic rewriting systems, recursion and extensional lambda calculi ⋮ Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus ⋮ Curry-Howard-Lambek correspondence for intuitionistic belief ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems
This page was built for publication:
