Well-founded recursion with copatterns and sized types
From MaRDI portal
Publication:5371960
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)
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
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