Friends with benefits. Implementing corecursion in foundational proof assistants
From MaRDI portal
Recommendations
- Foundational extensible corecursion: a proof assistant perspective
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- On the Foundations of Corecursion
- Mechanizing coinduction and corecursion in higher-order logic
- Using Structural Recursion for Corecursion
Cites work
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A Brief Overview of HOL4
- A fixedpoint approach to implementing (co)inductive definitions
- A note on model checking the modal \(\nu\)-calculus
- Abstract GSOS rules and a modular treatment of recursive definitions
- Automating theorem proving with SMT
- CIRC: A Behavioral Verification Tool Based on Circular Coinduction
- Coalgebraic bisimulation-up-to
- Code generation via higher-order rewrite systems
- Codifying guarded definitions with recursive schemes
- Coinduction All the Way Up
- Completely iterative algebras and completely iterative monads
- Compositional coinduction with sized types
- Containers: Constructing strictly positive types
- Copatterns, programming infinite structures by observations
- Fast Pattern Matching in Strings
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Formal Languages, Formally and Coinductively
- 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
- FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell
- HOL Light: An Overview
- scientific article; zbMATH DE number 2185691 (Why is no real title available?)
- scientific article; zbMATH DE number 4047683 (Why is no real title available?)
- scientific article; zbMATH DE number 3784244 (Why is no real title available?)
- scientific article; zbMATH DE number 1304993 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Indexed codata types
- Inductive and coinductive components of corecursive functions in Coq
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Language constructs for non-well-founded computation
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Mechanizing coinduction and corecursion in higher-order logic
- Parametric corecursion
- Parametricity in an impredicative sort
- Partial Recursive Functions in Higher-Order Logic
- Probabilistic functions and cryptographic oracles in higher order logic
- Productive coprogramming with guarded recursion
- Proofs for free. Parametricity for dependent types
- Recursive Functions on Lazy Lists via Domains and Topologies
- The Bird Tree
- The HOL-Omega Logic
- The Lean theorem prover (system description)
- The Matita interactive theorem prover
- The power of parameterization in coinductive proof
- Truly modular (co)datatypes for Isabelle/HOL
- Typed Lambda Calculi and Applications
- Well-founded recursion with copatterns and sized types
- Witnessing (co)datatypes
Cited in
(19)- A formalized general theory of syntax with bindings
- A formalized general theory of syntax with bindings: extended version
- Non-well-founded deduction for induction and coinduction
- CryptHOL: game-based proofs in higher-order logic
- Bisimulation and coinduction enhancements: a historical perspective
- Foundational extensible corecursion: a proof assistant perspective
- Friends with benefits. Implementing corecursion in foundational proof assistants
- AmiCo
- POPLMark reloaded: mechanizing proofs by logical relations
- Elaborating dependent (co)pattern matching: no pattern left behind
- Coinduction: automata, formal proof, companions (invited paper)
- scientific article; zbMATH DE number 7649955 (Why is no real title available?)
- Into the Infinite - Theory Exploration for Coinduction
- Up-to techniques for behavioural metrics via fibrations
- Formal definitions and proofs for partial (co)recursive functions
- A contextual formalization of structural coinduction
- Well-behaved (co)algebraic semantics of regular expressions in Dafny
- Nondeterministic asynchronous dataflow in Isabelle/HOL
- Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching
Describes a project that uses
Uses Software
This page was built for publication: Friends with benefits. Implementing corecursion in foundational proof assistants
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988636)
