지원사업
학술연구/단체지원/교육 등 연구자 활동을 지속하도록 DBpia가 지원하고 있어요.
커뮤니티
연구자들이 자신의 연구와 전문성을 널리 알리고, 새로운 협력의 기회를 만들 수 있는 네트워킹 공간이에요.
논문 기본 정보
- 자료유형
- 학술저널
- 저자정보
- 저널정보
- Korean Institute of Information Scientists and Engineers Journal of KIISE Journal of KIISE Vol.47 No.5
- 발행연도
- 2020.5
- 수록면
- 496 - 503 (8page)
- DOI
- 10.5626/JOK.2020.47.5.496
이용수
초록· 키워드
오류제보하기
람다나무문법 혹은 고차추상문법(HOAS)에 대한 일치화를 지원하는 Abella는 값호출(call-by-value) 계산방식으로 실행되는 System F<:의 순수한 부분에 대한 타입보존 기계증명 도전문제(POPLmark Challenge 2A)를 상당히 간결하게 해결할 수 있을 만큼 매력적인 장점을 지니는 증명도우미이다. 우리가 Abella를 이용해 특정 계산방식으로 한정하지 않은 일반적인 다형람다계산법(System F)의 타입보존 정리를 기계증명한 내용을 설명하고 이를 고차다형람다계산법(System Fω)의 타입보존정리에 대한 기계증명으로 확장하기 위해 진행 중인 연구를 보고한다.
목차
요약
Abstract
1. 서론
2. 다형타입람다계산법의 타입보존 기계증명
3. 고차다형타입람다계산법으로의 확장
4. 관련 연구
5. 결론 및 후속 연구
References
참고문헌 (7)
참고문헌 신청
D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang, "Abella: A system for reasoning about relational specifications," J. Formalized Reasoning, Vol. 7, No. 2, pp. 1-89, 2014.
A. Gacek, D. Miller, and G. Nadathur, "A two-level logic approach to reasoning about computations," Journal of Automated Reasoning, Vol. 49, pp. 241-273, Aug. 2012.
R. Pollack, "Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem," Unpublished note, Jan. 1995.
M. Takahashi, "Parallel reductions in λ-calculus," Inf. Comput., Vol. 118, pp. 120-127, Apr. 1995.
R. Horne, K. Y. Ahn, S.-W. Lin, and A. Tiu, "Quasi-open bisimilarity with mismatch is intuitionistic," Proc. of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, (New York, NY, USA), pp. 26-35, Association for Computing Machinery, 2018.
A. Gacek, D. Miller, and G. Nadathur, "A two-level logic approach to reasoning about computations," Journal of Automated Reasoning, Vol. 49, pp. 241-273, Aug. 2012.
R. Pollack, "Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem," Unpublished note, Jan. 1995.
M. Takahashi, "Parallel reductions in λ-calculus," Inf. Comput., Vol. 118, pp. 120-127, Apr. 1995.
R. Horne, K. Y. Ahn, S.-W. Lin, and A. Tiu, "Quasi-open bisimilarity with mismatch is intuitionistic," Proc. of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, (New York, NY, USA), pp. 26-35, Association for Computing Machinery, 2018.
함께 읽어보면 좋을 논문
논문 유사도에 따라 DBpia 가 추천하는 논문입니다. 함께 보면 좋을 연관 논문을 확인해보세요!
-
Mechanized Proof for Type Preservation of GTLC
Journal of KIISE
2019 .05
-
이더리움 지분증명으로의 전환
Proceedings of KIIT Conference
2022 .12
-
기존 연소계산법 검토 및 새로운 연소계산법 고찰
KOSCO SYMPOSIUM 논문집
2023 .05
-
람다 센서의 외부 오염에 따른 출력 데이터
대한설비공학회 학술발표대회논문집
2019 .06
-
람다 패시브하우스를 통해 살펴본 Energy# 적용 사례
태양에너지
2018 .06
-
Coinductive Subtyping for Recursive and Union Types
Journal of KIISE
2016 .12
-
Fitch에 의한 자연 연역법 증명을 Agda로 변환하기
한국정보기술학회논문지
2015 .01
-
블록체인 기반의 IOT 펌웨어에 적용가능한 지분, 신뢰, 작업 증명 방식에 대한 소고
Proceedings of KIIT Conference
2022 .06
-
스칼라의 대조 타입을 사용해 객체를 함수로 타입 안전하게 인코딩
한국정보과학회 학술발표논문집
2022 .12
-
비밀 공유 방식을 이용한 블록체인의 작업 증명
한국정보과학회 학술발표논문집
2020 .07
-
블록체인 기술을 활용한 컴퓨터 군사보안 적용 개념증명에 관한 연구
대한전기학회 학술대회 논문집
2018 .07
-
알루미늄/수소 기반 다형질 에너지물질 합성연구
한국추진공학회 학술대회논문집
2016 .12
-
전산유체해석을 통한 디퓨저타입과 패치타입 제품 이용 시 에센셜 오일의 흡입량 예측
한국산학기술학회 논문지
2022 .12
-
수학적 증명을 위한 대규모 언어모델 프롬프팅
한국정보과학회 학술발표논문집
2022 .12
-
블록체인의 합의 알고리즘 - 작업증명을 중심으로
한국컴퓨터정보학회 학술발표논문집
2020 .07
-
사우디 기후환경의 머신러닝 알고리즘 적용을 통한 실내 온열쾌적성 향상 및 냉방에너지 절감효과 분석
대한설비공학회 학술발표대회논문집
2024 .06
-
람다 모양 구조를 이용한 다방향 압전 에너지 하베스터
한국소음진동공학회 학술대회논문집
2020 .11
-
양자점 혼합에 따른 하이브리드 타입 광검출기 특성에 관한 연구
대한전자공학회 학술대회
2019 .06
-
Introduction to Error-Correction Codes Proof-of-Work
전자공학회지
2019 .05
이 논문의 저자 정보
이 논문과 함께 이용한 논문
최근 본 자료
댓글(0)
0