[Haskell'26] Lightning Talk: Formalizing explicit alpha-equivalence
ACM SIGPLAN · 10:07 · Watch on YouTube
Aaron Stump의 보스턴 칼리지 (자동 문서에서는 "Stone"으로 표기)는 Church의 1941년 람다 계산법의 명시적 알파-이름 바꾸기 단계가 형식적인 연구를 받을 자격이 있다고 주장합니다. 비록 논문들은 대개 이를 무시하고 정리 증명자들은 드브라인 지수로 이를 피하지만 말입니다. 그는 Agda로 형식화된 "알파 회피" 정리들을 제시합니다: 항의 결합 변수가 충분히 구별되면,...