The power of parameterization in coinductive proof
From MaRDI portal
Publication:2931796
DOI10.1145/2429069.2429093zbMath1301.68220MaRDI 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
simulation; compositionality; lattice theory; coinduction; interactive theorem proving; parameterized greatest fixed point
68N18: Functional programming and lambda calculus
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
06B99: Lattices
Related Items
Coinductive predicates and final sequences in a fibration, Unnamed Item, Unnamed Item, Unnamed Item, POPLMark reloaded: Mechanizing proofs by logical relations, Up-To Techniques for Behavioural Metrics via Fibrations, Tower Induction and Up-to Techniques for CCS with Fixed Points, Classical Logic with Mendler Induction, Mtac: A monad for typed tactic programming in Coq, Unnamed Item, Unnamed Item, Psi-calculi in Isabelle, Compositional Coinduction with Sized Types, Coinduction in Flow: The Later Modality in Fibrations, Paco, Coinductive predicates and final sequences in a fibration, Flag-based big-step semantics, Modular verification of programs with effects and effects handlers, (Co)inductive proof systems for compositional proofs in reachability logic, Non-well-founded deduction for induction and coinduction, Diacritical companions, Bisimulation and coinduction enhancements: a historical perspective, A Coinductive Animation of Turing Machines, On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions, Companions, Codensity and Causality, Generalizing Inference Systems by Coaxioms, Friends with Benefits, Unnamed Item
Uses Software
