Coinduction All the Way Up

DOI10.1145/2933575.2934564MaRDI QIDQ4635886zbMATH OpenOpenAlexFDO

Authors Damien Pous

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2933575.2934564

zbMATH Keywords

coinductioncomplete latticesGSOSenhancementsparameterized coinduction

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mechanization of proofs and logical operations (03B35) Complete lattices, completions (06B23)

Recommendations

• Probability all the way up
• A general account of coinduction up-to
• Coinduction up-to in a fibrational setting
• A note on FDE ``all the way up
• Practical coinduction
• Total logic
• Fully coherent inference

Cited in

(30)

• Companions, codensity and causality
• Companions, causality and codensity
• Corecursion up-to via causal transformations
• Bisimulation and coinduction enhancements: a historical perspective
• Into the Infinite - Theory Exploration for Coinduction
• (Co)inductive proof systems for compositional proofs in reachability logic
• Up-to techniques for behavioural metrics via fibrations
• Up-to techniques for branching bisimilarity
• Divergence and unique solution of equations
• Shall we juggle, coinductively?
• Bisimulations for delimited-control operators
• Tower induction and up-to techniques for CCS with fixed points
• Coinduction in Flow: The Later Modality in Fibrations
• Diacritical companions
• scientific article; zbMATH DE number 7407797 (Why is no real title available?)
• Compositional coinduction with sized types
• (Towards a) statistical probabilistic lazy lambda calculus
• Coinductive Proof Principles for Stochastic Processes
• Up-to techniques for behavioural metrics via fibrations
• A complete normal-form bisimilarity for algebraic effects and handlers
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• Strong induction is an up-to technique
• Divergence and unique solution of equations
• Coinductive algorithms for Büchi automata
• Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
• scientific article; zbMATH DE number 7649887 (Why is no real title available?)
• From bounded checking to verification of equivalence via symbolic up-to techniques
• Friends with benefits. Implementing corecursion in foundational proof assistants

Describes a project that uses

Uses Software

• CompCertTSO

This page was built for publication: Coinduction All the Way Up

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635886)