본 논문은 동형 암호화를 산술 또는 부울 연산을 넘어 직관주의 논리 증명 및 커리-하워드 대응에 따라 형식화된 함수형 프로그램 영역으로 확장하는 개념적 프레임워크를 제시한다. 산술 연산에 대한 잘 알려진 동형 암호화 방식을 검토한 후, 직관주의 논리에서 논리적 추론 단계를 지원하도록 유사한 개념을 적용하는 방법을 논의한다. 핵심은 논리 공식과 증명을 표현하고 조작하는 범주적 기반으로서의 다항식 函子와 경계된 자연 函子(BNF)이다. 부그래프 동형성 문제로부터의 환원을 통해 구성된 BNF 구별 문제라는 복잡도 이론적 어려움 가정을 개괄하여 암호화 보안의 기반을 제공한다. 마지막으로, 이러한 방법을 통해 전체 종속형 함수형 프로그램의 실행을 동형적으로 인코딩하는 방법을 설명하고, 소프트웨어 최적화 및 하드웨어 가속을 포함한 접근 방식의 효율성을 높이기 위한 전략을 개략적으로 설명한다.
