POPLmark 챌린지
POPLmark challenge |
프로그래밍 언어 이론에서 POPLmark 챌린지("Programming Languages benchmark" (이전의 Massechanized Metathory!) (Aydemir, 2005)는 프로그래밍 언어의 메타이론에서 자동화된 추론(또는 기계화)의 상태를 평가하고 토론과 조회를 촉진하기 위해 설계된 벤치마크 세트이다.형식적 방법 커뮤니티의 다양한 단면들 간의 애버레이션.간단히 말하면, 이 과제는 프로그램이 어떻게 동작할 것인지에 대한 사양과 얼마나 잘 일치하는지(그리고 이것이 수반하는 많은 복잡한 문제)를 측정하는 것입니다.이 도전은 펜실베니아 대학의 PL 클럽 회원들이 전 세계 협력자들과 협력하여 처음 제안했습니다.기계화 메타토리에 관한 워크숍은 이 과제에 참여하는 연구자들의 주요 회의입니다.
POPLmark 벤치마크 설계는 프로그래밍 언어에 대한 추론에 공통되는 기능에 의해 유도됩니다.이 과제에서는 대규모 프로그래밍 언어를 공식화할 필요는 없지만 다음과 같은 문제를 추론할 때는 정교함을 필요로 합니다.
- 바인딩
- 대부분의 프로그래밍 언어에는 단순한 유형의 람다 미적분 바인더에서 레코드 패턴 처리에 필요한 복잡하고 잠재적으로 무한 바인더까지 다양한 바인딩 형태가 있습니다.
- 인덕션
- 대상 감소 및 강력한 정규화와 같은 속성은 종종 복잡한 유도 인수를 요구한다.
- 재사용하다
- 콜라보레이션이 이 과제의 주요 목표인 솔루션에는 연구자가 매번 처음부터 시작할 필요 없이 언어 기능과 설계를 공유할 수 있는 재사용 가능한 컴포넌트가 포함될 것으로 예상됩니다.
문제
 | 이 섹션은 업데이트해야 합니다.하도록 이 . (2020년 3월) |
2007년 현재[update] POPLmark 챌린지는 세 부분으로 구성되어 있습니다.제1부에서는 시스템<: F(서브타이핑이 있는 시스템 F)의 유형만을 다루고 있으며 다음과 같은 문제가 있습니다.
파트 2는 시스템<: F의 구문과 의미론에 관한 것입니다.그것은 증거에 관한 것이다
파트 3은 시스템<: F의 공식화의 유용성에 관한 것이다.특히 이 과제에는 다음이 필요합니다.
- 운영 의미론 시뮬레이션 및 애니메이션화
- 형식화에서 유용한 알고리즘 추출
POPLmark 과제에는 다음 도구를 사용하여 몇 가지 해결 방법이 제안되었습니다.Isabelle/HOL, Twelf, Coq, αProlog, ATS, Abella 및 Matita.
「 」를 참조해 주세요.
레퍼런스
- 브라이언 E.아이데미르, 애런 보헤넌, 매튜 페어베언, J. 네이선 포스터, 벤자민 C 피어스, 피터 시웰, 디미트리오스 비티니오티스, 제프리 워시번, 스테파니 C 위리히, 그리고 스테판 A. 즈댄스윅.대중을 위한 기계화된 메타테고리:POPLmark 챌린지「고차 논리학의 정리 증명」, 제18회 국제 회의, 2005년, 컴퓨터 과학 강의 노트 제3603권, 50~65페이지.스프링거, 베를린/하이델베르크/뉴욕, 2005.
- 벤자민 C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic, It Is Language Metathory, In Bertrand Meyer, Jim Woodcock (Eds)확인된 소프트웨어: 이론, 도구, 실험, LNCS 4171, 스프링거 베를린 / 하이델베르크, 2008, 페이지 26~30, ISBN978-3-540-69147-1
