Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups

TL;DR

This work envisions extending homomorphic encryption beyond arithmetic to intuitionistic logic proofs and, via the Curry-Howard correspondence, to typed functional programs. It proposes a categorical framework using polynomial functors and bounded natural functors (BNFs) to encode and manipulate proofs, and introduces the BNF Distinguishing Problem as a hardness assumption grounded in Subgraph Isomorphism. The approach connects homomorphic encryption to the executable semantics of total, dependently typed languages (e.g., Idris) and flexible systems like MeTTa, with a concrete toy example illustrating encrypted function composition and modular arithmetic. While largely theoretical, the paper outlines concrete optimization avenues across software and hardware to bridge toward practical implementations and highlights formal future directions for strengthening security and efficiency.

Abstract

We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional programs. We begin by reviewing well-known homomorphic encryption schemes for arithmetic operations, and then discuss the adaptation of similar concepts to support logical inference steps in intuitionistic logic. Key to our construction are polynomial functors and Bounded Natural Functors (BNFs), which serve as a categorical substrate on which logic formulas and proofs are represented and manipulated. We outline a complexity-theoretic hardness assumption -- the BNF Distinguishing Problem, constructed via a reduction from Subgraph Isomorphism, providing a foundation for cryptographic security. Finally, we describe how these methods can homomorphically encode the execution of total, dependently typed functional programs, and outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.