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 latticesenhancementsGSOSparameterized coinduction

Mathematics Subject Classification ID

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

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)

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

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)