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