Friends with Benefits (Q2988636): Difference between revisions

@@ Property / author @@
-Andreas Lochbihler
@@ Property / author: Andreas Lochbihler / rank @@
-Normal rank
@@ Property / author @@
+Andreas Lochbihler
@@ Property / author: Andreas Lochbihler / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Matita
@@ Property / describes a project that uses: Matita / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL-Omega
@@ Property / describes a project that uses: HOL-Omega / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Paco
@@ Property / describes a project that uses: Paco / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MiniAgda
@@ Property / describes a project that uses: MiniAgda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Stern-Brocot Tree
@@ Property / describes a project that uses: Stern-Brocot Tree / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lean
@@ Property / describes a project that uses: Lean / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CIRC
@@ Property / describes a project that uses: CIRC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Haskell
@@ Property / describes a project that uses: Haskell / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Zero
@@ Property / describes a project that uses: HOL Zero / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Transfer
@@ Property / describes a project that uses: Transfer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lifting
@@ Property / describes a project that uses: Lifting / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOLCF
@@ Property / describes a project that uses: HOLCF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-662-54434-1_5
+Normal rank
@@ Property / OpenAlex ID @@
+W2595416494
@@ Property / OpenAlex ID: W2595416494 / rank @@
+Normal rank
@@ Property / cites work @@
+Containers: Constructing strictly positive types
@@ Property / cites work: Containers: Constructing strictly positive types / rank @@
+Normal rank
@@ Property / cites work @@
+Compositional Coinduction with Sized Types
@@ Property / cites work: Compositional Coinduction with Sized Types / rank @@
+Normal rank
@@ Property / cites work @@
+Well-founded recursion with copatterns and sized types
+Normal rank
@@ Property / cites work @@
+Copatterns
@@ Property / cites work: Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+The Matita Interactive Theorem Prover
@@ Property / cites work: The Matita Interactive Theorem Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Productive coprogramming with guarded recursion
@@ Property / cites work: Productive coprogramming with guarded recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs for free
@@ Property / cites work: Proofs for free / rank @@
+Normal rank
@@ Property / cites work @@
+Typed Lambda Calculi and Applications
@@ Property / cites work: Typed Lambda Calculi and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Inductive and Coinductive Components of Corecursive Functions in Coq
+Normal rank
@@ Property / cites work @@
+Friends with Benefits
@@ Property / cites work: Friends with Benefits / rank @@
+Normal rank
@@ Property / cites work @@
+Truly Modular (Co)datatypes for Isabelle/HOL
@@ Property / cites work: Truly Modular (Co)datatypes for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational extensible corecursion: a proof assistant perspective
+Normal rank
@@ Property / cites work @@
+Witnessing (Co)datatypes
@@ Property / cites work: Witnessing (Co)datatypes / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of Agda – A Functional Language with Dependent Types
+Normal rank
@@ Property / cites work @@
+Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Q5417200
@@ Property / cites work: Q5417200 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3962450
@@ Property / cites work: Q3962450 / rank @@
+Normal rank
@@ Property / cites work @@
+FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell
+Normal rank
@@ Property / cites work @@
+Codifying guarded definitions with recursive schemes
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q3784044
@@ Property / cites work: Q3784044 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024873
@@ Property / cites work: Q3024873 / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+The Bird Tree
@@ Property / cites work: The Bird Tree / rank @@
+Normal rank
@@ Property / cites work @@
+The HOL-Omega Logic
@@ Property / cites work: The HOL-Omega Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+The power of parameterization in coinductive proof
+Normal rank
@@ Property / cites work @@
+Language Constructs for Non-Well-Founded Computation
+Normal rank
@@ Property / cites work @@
+Q4649560
@@ Property / cites work: Q4649560 / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Pattern Matching in Strings
@@ Property / cites work: Fast Pattern Matching in Strings / rank @@
+Normal rank
@@ Property / cites work @@
+Partial Recursive Functions in Higher-Order Logic
@@ Property / cites work: Partial Recursive Functions in Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Theorem Proving with SMT
@@ Property / cites work: Automating Theorem Proving with SMT / rank @@
+Normal rank
@@ Property / cites work @@
+Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
+Normal rank
@@ Property / cites work @@
+Recursive Functions on Lazy Lists via Domains and Topologies
+Normal rank
@@ Property / cites work @@
+CIRC: A Behavioral Verification Tool Based on Circular Coinduction
+Normal rank
@@ Property / cites work @@
+Completely iterative algebras and completely iterative monads
+Normal rank
@@ Property / cites work @@
+Abstract GSOS Rules and a Modular Treatment of Recursive Definitions
+Normal rank
@@ Property / cites work @@
+Parametric corecursion
@@ Property / cites work: Parametric corecursion / rank @@
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+A fixedpoint approach to implementing (Co)inductive definitions
+Normal rank
@@ Property / cites work @@
+Mechanizing coinduction and corecursion in higher-order logic
+Normal rank
@@ Property / cites work @@
+Coinduction All the Way Up
@@ Property / cites work: Coinduction All the Way Up / rank @@
+Normal rank
@@ Property / cites work @@
+Coalgebraic Bisimulation-Up-To
@@ Property / cites work: Coalgebraic Bisimulation-Up-To / rank @@
+Normal rank
@@ Property / cites work @@
+Q4251915
@@ Property / cites work: Q4251915 / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Indexed codata types
@@ Property / cites work: Indexed codata types / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Languages, Formally and Coinductively
@@ Property / cites work: Formal Languages, Formally and Coinductively / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
+Normal rank
@@ Property / cites work @@
+A note on model checking the modal \(\nu\)-calculus
+Normal rank