A case study in programming coinductive proofs: Howe’s method
From MaRDI portal
Publication:5236557
DOI10.1017/S0960129518000415zbMath1430.68418OpenAlexW2899165262WikidataQ113857439 ScholiaQ113857439MaRDI QIDQ5236557
Alberto Momigliano, David Thibodeau, Brigitte Pientka
Publication date: 9 October 2019
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129518000415
Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Formal Reasoning Using Distributed Assertions ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Mechanized metatheory revisited ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Verifying termination and reduction properties about higher-order logic programs
- Fully abstract models of typed \(\lambda\)-calculi
- Formal foundations of operational semantics
- \(\pi\)-calculus in (Co)inductive-type theory
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Proving congruence of bisimulation in functional programming languages
- Cut elimination for a logic with induction and co-induction
- Strongly typed term representations in Coq
- A domain equation for bisimulation
- Syntactic Logical Relations for Polymorphic and Recursive Types
- Programming with Higher-Order Logic
- Copatterns
- Programming with binders and indexed data-types
- Proof search specifications of bisimulation and modal logics for the π-calculus
- Indexed codata types
- Towards a mechanized metatheory of standard ML
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Formalising the pi-calculus using nominal logic
- Inductive Beluga: Programming Proofs
- A framework for defining logics
- αCheck: A mechanized metatheory model checker
- Mechanizing proofs with logical relations – Kripke-style
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Equivalence in functional languages with effects
- Abella: A System for Reasoning about Relational Specifications
- Wellfounded recursion with copatterns
- A proof theory for generic judgments
- Contextual modal type theory
- Well-founded recursion with copatterns and sized types
- Howe's method for higher-order languages
- Types for Proofs and Programs
- Higher-order psi-calculi
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Psi-calculi in Isabelle
- Programming Languages and Systems
This page was built for publication: A case study in programming coinductive proofs: Howe’s method
