가역적 중간 언어 L4, 그 타입 시스템 및 양방향 작은 단계 의미론

요약

L4는 가역적이고 선형 타입의 저수준 중간 언어로, 가역 프로그래밍 언어를 컴파일하기 위해 설계되었습니다. 본 논문은 L4에 대한 공식적인 타입 시스템과 양방향 작은 단계 의미론을 제시합니다. 이 의미론은 실행 방향(순전 또는 역전)이 결정되고 변경될 수 있다는 특징을 다룹니다.

핵심 포인트

• L4는 가역적이고 선형 타입을 가진 저수준 중간 언어입니다.
• 가역 프로그래밍 컴파일러를 위한 핵심 목표로 제시됩니다.
• 공식 타입 시스템과 양방향 작은 단계 의미론을 정의했습니다.
• 실행 방향(순전/역전)이 동적으로 변경될 수 있습니다.