Equational Reasoning with Applicative Functors

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

Authors: 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

Recommendations

• Equational reasoning in Isabelle
• Publication:2754042
• Equational type logic
• scientific article; zbMATH DE number 1552533
• Equational systems of functors
• scientific article; zbMATH DE number 139986
• Equational theories for inductive types
• Equational presentations of functors and monads
• Equational coalgebraic logic
• Equational semantics

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

• 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
• Title not available (Why is that?)
• 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

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)