Mixed Inductive/Coinductive Types and Strong Normalization
From MaRDI portal
Publication:3498444
DOI10.1007/978-3-540-76637-7_19zbMath1138.68023OpenAlexW1523149969MaRDI QIDQ3498444
Publication date: 15 May 2008
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-76637-7_19
Related Items (4)
Polarized subtyping ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Sound and complete equational reasoning over comodels ⋮ Compositional Coinduction with Sized Types
Cites Work
- Unnamed Item
- Unnamed Item
- Recursive programming with proofs
- Iteration and coiteration schemes for higher-order and nested datatypes
- Inductive types and type constraints in the second-order lambda calculus
- Polarized Subtyping for Sized Types
- Strong Normalization and Equi-(Co)Inductive Types
- Towards Generic Programming with Sized Types
- Proofs of strong normalisation for second order classical natural deduction
- Type-based termination of recursive definitions
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- On the Stability by Union of Reducibility Candidates
- Semi-continuous Sized Types and Termination
This page was built for publication: Mixed Inductive/Coinductive Types and Strong Normalization
