LFPL: 재검토 및 기계화

요약

본 논문은 아핀 타입 시스템을 활용하여 다항 시간 내 계산 가능한 함수를 특징짓는 LFPL 언어와 그 메타 이론을 현대적으로 재정립하고 기계화합니다. 기존의 복잡한 건전성 및 완전성 증명을 간소화하여 접근성을 높였으며, 이를 증명 보조기인 Istari를 통해 기계화한 첫 번째 사례 연구를 제시합니다.

핵심 포인트

• LFPL의 건전성 증명을 위해 LFPL+를 대상으로 빅스텝 비용 의미론 기반의 명시적 다항식 구축 기법을 적용함
• 완전성 증명 과정에서 퍼스트 클래스 함수와 리스트 기반의 새로운 스택 구조를 도입하여 논증을 단순화함
• 다항 시간 튜닝 머신을 제한된 선형 함수와 리스트만으로 시뮬레이션할 수 있음을 입증함
• 최신 증명 보조기인 Istari를 사용하여 LFPL의 메타 이론을 성공적으로 기계화함