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
