Key points are not available for this paper at this time.
매개변수성은 동일한 데이터 구조의 서로 다른 구현 간에 증명을 전송할 수 있게 합니다. λΠ-계산 모듈 이론은 의존 타입과 사용자 정의 재작성 규칙을 갖는 λ-계산의 확장입니다. 이는 서로 다른 증명 시스템 간에 증명을 교환하기 위해 사용되는 논리적 프레임워크입니다. 우리는 매개변수성에서 영감을 받은 λΠ-계산 모듈 이론의 이론 해석을 정의합니다. 이러한 해석은 소스 이론을 대상 이론에 포함할 수 있을 때, 명제와 증명 개념을 갖춘 이론 간에 무료로 증명을 전송할 수 있도록 합니다.
토마스 트라베르시(Tomas Traversié, Mon)는 이 문제를 연구했습니다.