Well-founded recursion with copatterns and sized types

DOI10.1017/S0956796816000022zbMath1420.68031MaRDI QIDQ5371960

Andreas Abel, Brigitte Pientka

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Related Items

Unnamed Item, Is sized typing for Coq practical?, Into the Infinite - Theory Exploration for Coinduction, Polarized subtyping, Unnamed Item, Unnamed Item, Friends with Benefits, Temporal refinements for guarded recursive types, (Co)inductive proof systems for compositional proofs in reachability logic, Unnamed Item, Non-well-founded deduction for induction and coinduction, A case study in programming coinductive proofs: Howe’s method, Integrating induction and coinduction via closure operators and proof cycles, Causal computational complexity of distributed processes

Uses Software

• Coq
• Agda
• MiniAgda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependent types for program termination verification
• Copatterns
• Representations of Stream Processors Using Nested Fixed Points
• Semantic types
• Polarised subtyping for sized types
• Type-Based Termination with Sized Products
• Type-based termination of recursive definitions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
• Intuitionistic sets and ordinals
• Typed Lambda Calculi and Applications
• Semi-continuous Sized Types and Termination
• Rewriting Techniques and Applications