Friends with Benefits

DOI10.1007/978-3-662-54434-1_5zbMath1485.68280OpenAlexW2595416494MaRDI QIDQ2988636

Jasmin Christian Blanchette, Dmitriy Traytel, Andrei Popescu, Aymeric Bouzy, Andreas Lochbihler

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_5

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

CryptHOL: game-based proofs in higher-order logic, A formalized general theory of syntax with bindings, Into the Infinite - Theory Exploration for Coinduction, POPLMark reloaded: Mechanizing proofs by logical relations, Elaborating dependent (co)pattern matching: No pattern left behind, Unnamed Item, Unnamed Item, Up-to techniques for behavioural metrics via fibrations, Friends with Benefits, A formalized general theory of syntax with bindings: extended version, Bisimulation and coinduction enhancements: a historical perspective, Non-well-founded deduction for induction and coinduction, AmiCo

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• Haskell
• Isabelle/ZF
• HOL
• Matita
• CIRC
• HOL Light
• HOL-Omega
• Agda
• Paco
• Lean
• HOL Zero
• Transfer
• Lifting
• MiniAgda
• HOLCF
• Stern-Brocot Tree
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A note on model checking the modal \(\nu\)-calculus
• Isabelle/HOL. A proof assistant for higher-order logic
• Completely iterative algebras and completely iterative monads
• Containers: Constructing strictly positive types
• Witnessing (Co)datatypes
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Proofs for free
• Abstract GSOS Rules and a Modular Treatment of Recursive Definitions
• Inductive and Coinductive Components of Corecursive Functions in Coq
• Truly Modular (Co)datatypes for Isabelle/HOL
• Recursive Functions on Lazy Lists via Domains and Topologies
• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• Coalgebraic Bisimulation-Up-To
• Copatterns
• The power of parameterization in coinductive proof
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Foundational extensible corecursion: a proof assistant perspective
• Indexed codata types
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Friends with Benefits
• HOL Light: An Overview
• A Brief Overview of Agda – A Functional Language with Dependent Types
• The HOL-Omega Logic
• The Lean Theorem Prover (System Description)
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• A Brief Overview of HOL4
• Code Generation via Higher-Order Rewrite Systems
• Partial Recursive Functions in Higher-Order Logic
• The Bird Tree
• Fast Pattern Matching in Strings
• Mechanizing coinduction and corecursion in higher-order logic
• Coinduction All the Way Up
• The Matita Interactive Theorem Prover
• A fixedpoint approach to implementing (Co)inductive definitions
• Productive coprogramming with guarded recursion
• Language Constructs for Non-Well-Founded Computation
• Automating Theorem Proving with SMT
• Formal Languages, Formally and Coinductively
• Well-founded recursion with copatterns and sized types
• Typed Lambda Calculi and Applications
• FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell
• Compositional Coinduction with Sized Types
• Parametric corecursion
• Codifying guarded definitions with recursive schemes