Effect polymorphism in higher-order logic (proof pearl)

DOI10.1007/978-3-319-66107-0_25zbMath1468.68061OpenAlexW2746834364MaRDI QIDQ5915785

Andreas Lochbihler

Publication date: 4 January 2018

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

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_25

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 (3)

Effect polymorphism in higher-order logic (proof pearl) ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Monomorphic Monad

Uses Software

• Isabelle/HOL
• HOL
• Locales

Cites Work

• 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
• 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)