Equational Reasoning with Applicative Functors

DOI10.1007/978-3-319-43144-4_16zbMath1464.68063OpenAlexW2506655188MaRDI QIDQ2829262

Joshua Schneider, Andreas Lochbihler

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_16

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) General theory of categories and functors (18A99) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Quotients of Bounded Natural Functors ⋮ Unnamed Item ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Equational Reasoning with Applicative Functors

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• HOL
• HOL-Omega
• Transfer
• Lifting
• Stern-Brocot Tree
• Applicative Lifting
• Meta Model Isabelle
• Archive Formal Proofs
• Density Compiler

Cites Work

• Unnamed Item
• A higher-order implementation of rewriting
• Lambda terms definable as combinators
• More Church-Rosser proofs (in Isabelle/HOL)
• A Verified Compiler for Probability Density Functions
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Equational Reasoning with Applicative Functors
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Nonfree Datatypes in Isabelle/HOL
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• The HOL-Omega Logic
• Imperative Functional Programming with Isabelle/HOL
• The Bird Tree
• Just do it
• Applicative programming with effects

This page was built for publication: Equational Reasoning with Applicative Functors