Effect polymorphism in higher-order logic (proof pearl)

DOI10.1007/s10817-018-9476-2zbMath1468.68062OpenAlexW2855026817WikidataQ129563246 ScholiaQ129563246MaRDI QIDQ5919584

Andreas Lochbihler

Publication date: 21 August 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9476-2

zbMATH Keywords

effectspolymorphismequational reasoningmonadIsabelle/HOLmonad transformer

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Quotients of Bounded Natural Functors ⋮ Unnamed Item

Uses Software

• Isabelle
• Haskell
• HOL
• HOL-Omega
• Locales
• Transfer
• Lifting
• Tycon
• Zoo Probabilistic Systems
• Monomorphic Monad
• Density Compiler

Cites Work

• Unnamed Item
• The coinductive resumption monad
• A framework for developing stand-alone certifiers
• Verified memoization and dynamic programming
• Locales: a module system for mathematical theories
• A Verified Compiler for Probability Density Functions
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Equational Reasoning with Applicative Functors
• Truly Modular (Co)datatypes for Isabelle/HOL
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Concrete Semantics
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Formalized Hierarchy of Probabilistic System Types
• The HOL-Omega Logic
• Imperative Functional Programming with Isabelle/HOL
• The Essence of Multitasking
• Refinement Calculus
• Higher-order functions for parsing
• Formal verification of monad transformers
• Just do it
• Stochastic lambda calculus and monads of probability distributions
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell
• Effect polymorphism in higher-order logic (proof pearl)

This page was built for publication: Effect polymorphism in higher-order logic (proof pearl)