Effect polymorphism in higher-order logic (proof pearl)
From MaRDI portal
Publication:5919584
DOI10.1007/s10817-018-9476-2zbMath1468.68062OpenAlexW2855026817WikidataQ129563246 ScholiaQ129563246MaRDI QIDQ5919584
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
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)
Uses Software
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)