A contextual formalization of structural coinduction
From MaRDI portal
Cites work
- A coalgebraic decision procedure for NetKAT
- A lattice-theoretical fixpoint theorem and its applications
- A new type assignment for λ-terms
- A note on logical relations between semantics and syntax
- A semantic model of types and machine instructions for proof-carrying code
- Abstracting models of strong normalization for classical calculi
- An application of co-inductive types in Coq: verification of the alternating bit protocol
- Checking NFA equivalence with bisimulations up to congruence
- Circular coinduction in Coq using bisimulation-up-to techniques
- Classical (co)recursion: Mechanics
- Copatterns, programming infinite structures by observations
- Enhancements of the bisimulation proof method
- Focalisation and Classical Realisability
- Foundational extensible corecursion: a proof assistant perspective
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Hidden coinduction: behavioural correctness proofs for objects
- scientific article; zbMATH DE number 5851813 (Why is no real title available?)
- scientific article; zbMATH DE number 4047683 (Why is no real title available?)
- scientific article; zbMATH DE number 3707731 (Why is no real title available?)
- scientific article; zbMATH DE number 3596799 (Why is no real title available?)
- scientific article; zbMATH DE number 1241702 (Why is no real title available?)
- scientific article; zbMATH DE number 1479631 (Why is no real title available?)
- scientific article; zbMATH DE number 819768 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Incremental pattern-based coinduction for process algebra and its Isabelle formalization
- Intensional interpretations of functionals of finite type I
- Linear logic
- Logical relations and the typed λ-calculus
- On a hitherto unexploited extension of the finitary standpoint
- On coinductive equivalences for higher-order probabilistic functional programs
- On the interpretation of intuitionistic number theory
- Parametric polymorphism and operational equivalence
- Practical coinduction
- Practical foundations for programming languages
- Proof methods for corecursive programs
- Proving Properties of Programs by Structural Induction
- Regular expression containment, coinductive axiomatization and computational interpretation
- Structures for structural recursion
- The duality of classical intersection and union types
- The duality of computation
- The generic approximation lemma
- The marriage of bisimulations and Kripke logical relations
- The power of parameterization in coinductive proof
- Truly modular (co)datatypes for Isabelle/HOL
- Types and programing languages
- Un théorème sur les fonctions d'ensembles.
This page was built for publication: A contextual formalization of structural coinduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6946025)
