Inductive Types and Type Constraints in the Second-Order lambda Calculus
By N. Mendler. 1991
Abstract Mendler, N.P., Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic 51 (1991) 159–172. We add to the second-order lambda calculus the type constructors μ and ν, which give the least and greatest solutions to positively defined type expressions. Strong normalizability of typed terms is shown using Girard's candidat de reductibilite method. Using the same structure built for that proof, we prove a necessary and sufficient condition for determining when a collection of equational type constraints admit the typing of only strongly normalizable terms.
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
Citations in the corpus
- Heterogeneous substitution systems revisited (2016, neutral): “The notion of category is actually more refined in [7]; two conditions must be satisfied by a category: (i) Its hom-types C ( a, b ) need to be sets .”
- Iteration and coiteration schemes for higher-order and nested datatypes (2005, methodology): “In Mendler’s original system[40] as well as its variant for the treatment of primitive (co)recursion[39], positivity of F is always required, which is a very natural concept in the case = ∗.”
- Termination checking with types (2004, methodology): “Relative to their work, the novel contributions of this article are: (1) An informal introduction into type based termination, starting with its simplest form, Mendler’s rule for recursion [ 35 ], and ending with our restriction of Gim´ enez’ system.”