Inductive types and type constraints in the second-order lambda calculus
From MaRDI portal
Publication:2639842
DOI10.1016/0168-0072(91)90069-XzbMath0719.03008OpenAlexW2003295197MaRDI QIDQ2639842
Publication date: 1991
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0168-0072(91)90069-x
Related Items
Classical Logic with Mendler Induction ⋮ Size-based termination of higher-order rewriting ⋮ Mixed Inductive/Coinductive Types and Strong Normalization ⋮ A realizability interpretation of Church's simple theory of types ⋮ Unnamed Item ⋮ Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications ⋮ Strong normalization results by translation ⋮ Unifying structured recursion schemes ⋮ Unnamed Item ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Unnamed Item ⋮ Intuitionistic fixed point logic ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ The Recursion Scheme from the Cofree Recursive Comonad ⋮ Termination checking with types ⋮ Compositional Coinduction with Sized Types ⋮ Iteration and coiteration schemes for higher-order and nested datatypes ⋮ Logic of subtyping ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ Undecidability of equality for codata types ⋮ Corecursion and Non-divergence in Session-Typed Processes ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ Implementing a normalizer using sized heterogeneous types ⋮ Structures definable in polymorphism ⋮ Semantical analysis of perpetual strategies in \(\lambda\)-calculus ⋮ Modular Dependent Induction in Coq, Mendler-Style ⋮ From signatures to monads in \textsf{UniMath} ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles ⋮ Heterogeneous Substitution Systems Revisited ⋮ On modal logics of partial recursive functions
Cites Work
