Syntactic Effectful Realizability in Higher-Order Logic

TL;DR

This paper introduces EffHOL, a new higher-order logic framework that incorporates effects via monads into realizability, enabling the extraction of effectful realizers and unifying various computational paradigms.

Contribution

EffHOL extends syntactic realizability to support effectful computations, combining higher-kinded polymorphism with monadic effects, and provides a constructive translation from HOL.

Findings

EffHOL can synthesize effectful realizers for unprovable propositions in pure HOL.

Examples include continuations and memoization demonstrating diverse computational models.

EffHOL induces an evidenced frame, tripos, and realizability topos, connecting syntax and semantics.

Abstract

Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that handles realizability as a syntactic translation of propositions into new propositions that describe what it means to realize the input proposition. This paper introduces EffHOL (Effectful Higher-Order Logic), a novel framework that expands syntactic realizability to uniformly support modern programming paradigms with side effects. EffHOL combines higher-kinded polymorphism, enabling typing of realizers for higher-order propositions, with a computational term language that uses monads to represent and reason about effectful computations. We craft a syntactic realizability translation from (intuitionistic) higher-order logic (HOL) to EffHOL, ensuring the extraction of computable realizers through a constructive soundness proof. EffHOL's parameterization by monads allows for the synthesis of effectful realizers for propositions unprovable in pure HOL, bridging the gap between traditional and effectful computational paradigms. Examples, including continuations and memoization, showcase EffHOL's capability to unify diverse computational models, with traditional ones as special cases. For a semantic connection, we show that any instance of EffHOL induces an evidenced frame, which, in turn, yields a tripos and a realizability topos.