Mixed Inductive/Coinductive Types and Strong Normalization

DOI10.1007/978-3-540-76637-7_19zbMath1138.68023OpenAlexW1523149969MaRDI QIDQ3498444

Andreas Abel

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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