The power of parameterization in coinductive proof
From MaRDI portal
Recommendations
- A coinductive approach to proof search
- Parameterized provability in equational logic
- scientific article; zbMATH DE number 3880082
- Proof by computation in the Coq system
- Proofs in parameterized specifications
- scientific article; zbMATH DE number 1761886
- Some definitorial suggestions for parameterized proof complexity
- Paramodulation-based theorem proving
- Parameterized proof complexity
- A proof of Moessner's theorem by coinduction
Cited in
(39)- 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
- Paco
- Coinductive predicates and final sequences in a fibration
- 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. Implementing corecursion in foundational proof assistants
- scientific article; zbMATH DE number 7037626 (Why is no real title available?)
- Proof-Relevant Parametricity
- Coinductive predicates and final sequences in a fibration
- Up-to techniques for behavioural metrics via fibrations
- Foundations of regular coinduction
- scientific article; zbMATH DE number 7559481 (Why is no real title available?)
- POPLMark reloaded: mechanizing proofs by logical relations
- scientific article; zbMATH DE number 7407797 (Why is no real title available?)
- Flag-based big-step semantics
- Using a generalisation critic to find bisimulations for coinductive proofs
- 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
- Compositional coinduction with sized types
- Coinduction: automata, formal proof, companions (invited paper)
- Coinduction in Flow: The Later Modality in Fibrations
- scientific article; zbMATH DE number 7649963 (Why is no real title available?)
- Psi-calculi in Isabelle
- Up-to techniques for behavioural metrics via fibrations
- Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
- Completeness of asynchronous session tree subtyping in Coq
- Relative security: (dis)proving resilience against semantic optimization vulnerabilities in Isabelle/HOL. Extended version
- Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
- A contextual formalization of structural coinduction
- A sound and complete projection for global types
- Formalising subject reduction and progress for multiparty session processes
- Formalising asynchronous session subtyping
This page was built for publication: The power of parameterization in coinductive proof
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931796)
