확률적 Iris를 향한 첫 걸음: 독립성, 조건부 확률, 그리고 동적 힙 할당의 조화

요약

본 논문은 동적 메모리 할당을 지원하면서 독립성과 조건부 확률 추론이 가능한 최초의 범용 확률 논리(GPL)인 Amaryllis를 제안합니다. 기존 GPL이 해결하지 못했던 포인터 소유권과 확률적 추론 간의 충돌 문제를 '인덱스된 가치 평가' 모델을 통해 해결하였으며, 이를 Rocq 증명 보조기에서 기계화하는 데 성공했습니다.

핵심 포인트

• Amaryllis는 동적 힙 할당과 확률적 독립성/조건부 추론을 결합한 최초의 GPL입니다.
• 인덱스된 가치 평가(indexed valuation) 모델을 도입하여 분포 수준의 자원 소유권을 정의했습니다.
• Iris의 핵심 개념인 프레임 보존 업데이트와 권위 있는 자원 대수를 확률적 추론에 맞게 적응시켰습니다.
• 모든 연구 결과를 Rocq 증명 보조기를 통해 기계화하여 검증 가능성을 확보했습니다.