Lean에서의 다중 정렬 하이브리드 다항 양상 논리 (Many-Sorted Hybrid Polyadic Modal Logic) 형식화

우리는 다중 정렬 시그니처 (many-sorted signatures)와 다항 양상 연산자 (polyadic modal operators)를 갖춘 일반적인 하이브리드 양상 논리 (hybrid modal logic)의 Lean 형식화를 제시합니다. 이 시스템은 대수적 명세 (algebraic specification)와 동적 논리 (dynamic logics)의 아이디어를 모두 차용하였으며, 프로그래밍 언어와 보안 프로토콜을 명세하고 검증하기 위한 통일된 공리적 기반 (axiomatic foundation) 역할을 하도록 설계되었습니다. 우리는 사용자가 언어와 프로토콜을 다중 정렬 시그니처로 정의하고, 관련 도메인 특화 공리 (domain-specific axioms)를 명시하며, 프로그램 실행 또는 프로토콜 실행에 대해 추론할 수 있도록 하는 DSL을 제공합니다. 우리는 이 시스템의 건전성 정리 (soundness theorem)에 대한 기계 검증된 증명을 제공하며, 다음과 같은 여러 응용 사례를 통해 프레임워크의 다재다능함을 보여줍니다: 코드 검증을 위한 명령형 프로그래밍 언어, 보안 프로토콜을 위한 BAN 논리, 그리고 양상 체계 S5입니다. 우리는 우리의 형식화가 본질적으로 정렬되도록 (intrinsically sorted) 설계했습니다. 즉, 기본 언어에서의 well-sorted 공식은 Lean에서의 well-typed 항 (terms)이 됩니다. 이러한 본질적 정렬 덕분에, 모든 도메인 특화 응용 프로그램은 사용자가 증명하는 데 추가적인 구문론적 오버헤드(syntactic overhead)를 요구하지 않고 DSL을 통해 우리 프레임워크에 쉽게 임베딩될 수 있습니다. 이 논문에서 제시된 모든 코드는 다음 저장소에서 공개적으로 접근할 수 있습니다: https://github.com/alexoltean61/msphml-lean