Equational Reasoning with Applicative Functors

DOI10.1007/978-3-319-43144-4_16zbMATH Open1464.68063OpenAlexW2506655188MaRDI QIDQ2829262FDOQ2829262

Andreas Lochbihler, Joshua Schneider

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)

Cites Work

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

Cited In (10)

• APLicative Programming with Naperian Functors
• Title not available (Why is that?)
• Just do it
• Variadic equational matching in associative and commutative theories
• Quotients of Bounded Natural Functors
• Title not available (Why is that?)
• Equational Reasoning with Applicative Functors
• Title not available (Why is that?)
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)

Uses Software

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

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Equational presentations of functors and monads 👍 👎
• Equational reasoning in Isabelle 👍 👎
• Equational theories for inductive types 👍 👎
• Equational coalgebraic logic 👍 👎
• Equational type logic 👍 👎
• Equational semantics 👍 👎
• Equational systems of functors 👍 👎

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829262)