The power of parameterization in coinductive proof

DOI10.1145/2429069.2429093zbMath1301.68220OpenAlexW2014364142MaRDI QIDQ2931796

Viktor Vafeiadis, Georg Neis, Derek R. Dreyer, Chung-Kil Hur

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

simulationcompositionalitylattice theorycoinductioninteractive theorem provingparameterized greatest fixed point

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Lattices (06B99)

Related Items (29)

Coinductive predicates and final sequences in a fibration ⋮ Tower Induction and Up-to Techniques for CCS with Fixed Points ⋮ Classical Logic with Mendler Induction ⋮ Diacritical companions ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Up-to techniques for behavioural metrics via fibrations ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Psi-calculi in Isabelle ⋮ Companions, Codensity and Causality ⋮ Generalizing Inference Systems by Coaxioms ⋮ Friends with Benefits ⋮ Unnamed Item ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Up-To Techniques for Behavioural Metrics via Fibrations ⋮ Flag-based big-step semantics ⋮ Modular verification of programs with effects and effects handlers ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ Unnamed Item ⋮ Compositional Coinduction with Sized Types ⋮ Unnamed Item ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ A Coinductive Animation of Turing Machines ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Non-well-founded deduction for induction and coinduction ⋮ Paco ⋮ Coinductive predicates and final sequences in a fibration ⋮ Unnamed Item

Uses Software

• Coq
• Isabelle

This page was built for publication: The power of parameterization in coinductive proof