Compositional Coinduction with Sized Types

DOI10.1007/978-3-319-40370-0_2zbMath1475.68073OpenAlexW2500784495MaRDI QIDQ5739446

Andreas Abel

Publication date: 15 July 2016

Published in: Coalgebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01446030/file/418352_1_En_2_Chapter.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Friends with Benefits

Uses Software

• Coq
• Paco

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive types and type constraints in the second-order lambda calculus
• A predicative analysis of structural recursion
• The power of parameterization in coinductive proof
• Foundational extensible corecursion: a proof assistant perspective
• Mixed Inductive/Coinductive Types and Strong Normalization
• Subtyping, Declaratively
• Type-based termination of recursive definitions
• Wellfounded recursion with copatterns
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• The Size-Change Termination Principle for Constructor Based Languages
• Enhancements of the bisimulation proof method
• Semi-continuous Sized Types and Termination

This page was built for publication: Compositional Coinduction with Sized Types