A case study in programming coinductive proofs: Howe's method
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1670817 (Why is no real title available?)
- scientific article; zbMATH DE number 1231524 (Why is no real title available?)
- scientific article; zbMATH DE number 1241702 (Why is no real title available?)
- scientific article; zbMATH DE number 1082078 (Why is no real title available?)
- scientific article; zbMATH DE number 1424019 (Why is no real title available?)
- scientific article; zbMATH DE number 2238212 (Why is no real title available?)
- A domain equation for bisimulation
- A framework for defining logics
- A hybrid encoding of Howe's method for establishing congruence of bisimilarity
- A proof theory for generic judgments
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Abella: a system for reasoning about relational specifications
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Contextual modal type theory
- Copatterns, programming infinite structures by observations
- Cut elimination for a logic with induction and co-induction
- Equivalence in functional languages with effects
- Formal foundations of operational semantics
- Formalising the pi-calculus using nominal logic
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Fully abstract models of typed \(\lambda\)-calculi
- Higher-order psi-calculi
- Howe's method for higher-order languages
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Index-stratified types
- Indexed codata types
- Inductive beluga: programming proofs
- Mechanizing proofs with logical relations -- Kripke-style
- Programming Languages and Systems
- Programming with binders and indexed data-types
- Programming with higher-order logic.
- Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
- Proving congruence of bisimulation in functional programming languages
- Psi-calculi in Isabelle
- Strongly typed term representations in Coq
- Syntactic logical relations for polymorphic and recursive types
- Towards a mechanized metatheory of Standard ML
- Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
- Types for Proofs and Programs
- Verifying termination and reduction properties about higher-order logic programs
- Well-founded recursion over contextual objects
- Well-founded recursion with copatterns and sized types
- Wellfounded recursion with copatterns: a unified approach to termination and productivity
- -calculus in (Co)inductive-type theory
- αCheck: A mechanized metatheory model checker
Cited in
(12)- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- scientific article; zbMATH DE number 1424019 (Why is no real title available?)
- Infinitary Howe's method
- Mechanized metatheory revisited
- \(\mathrm{HO}\pi\) in Coq
- Inductive beluga: programming proofs
- Programming inductive proofs. A new approach based on contextual types
- POPLMark reloaded: mechanizing proofs by logical relations
- Formal Reasoning Using Distributed Assertions
- A hybrid encoding of Howe's method for establishing congruence of bisimilarity
- Mechanizing proofs with logical relations -- Kripke-style
- Studying a Range Proof Technique — Exception and Optimisation
This page was built for publication: A case study in programming coinductive proofs: Howe's method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5236557)
