Friends with Benefits
From MaRDI portal
Publication:2988636
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
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
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
