Equational Reasoning with Applicative Functors

DOI10.1007/978-3-319-43144-4_16MaRDI QIDQ2829262zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Equational reasoning in Isabelle
• scientific article; zbMATH DE number 1670742
• 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

Cites work

• scientific article; zbMATH DE number 3071073 (Why is no real title available?)
• A higher-order implementation of rewriting
• A verified compiler for probability density functions
• Applicative programming with effects
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Equational Reasoning with Applicative Functors
• Imperative Functional Programming with Isabelle/HOL
• Just do it
• Lambda terms definable as combinators
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• More Church-Rosser proofs (in Isabelle/HOL)
• Nonfree datatypes in Isabelle/HOL. Animating a many-sorted metatheory
• Probabilistic functions and cryptographic oracles in higher order logic
• The Bird Tree
• The HOL-Omega Logic

Cited in

(11)

• APLicative Programming with Naperian Functors
• scientific article; zbMATH DE number 1670742 (Why is no real title available?)
• Just do it
• Variadic equational matching in associative and commutative theories
• Quotients of Bounded Natural Functors
• scientific article; zbMATH DE number 7471712 (Why is no real title available?)
• Equational Reasoning with Applicative Functors
• scientific article; zbMATH DE number 7523908 (Why is no real title available?)
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)
• A practical formalization of monadic equational reasoning in dependent-type theory

Describes a project that uses

Uses Software

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

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)