サインイン
インサイト - 양자 프로그래밍
양자 Hoare 논리의 상대적 완전성에 대하여
이 논문은 만족 기반 양자 Hoare 논리의 상대적 완전성을 증명하였다. 이를 위해 먼저 결정론적 단언과 양자 프로그램으로 구성된 Hoare 삼중체의 의미론과 증명 시스템을 수립하였다. 그리고 결정론적 단언의 최약 선행 조건을 활용하여 확률적 표현의 최약 선행 용어 계산을 구축하였다. 이를 통해 양자 Hoare 논리의 상대적 완전성을 도출하였다.
양자 회로의 재귀적 정의에 대한 검증
이 논문에서는 재귀적으로 정의된 양자 회로의 정확성을 공식적으로 검증하기 위한 증명 시스템을 제시한다. 이 증명 시스템의 건전성과 (상대적) 완전성을 입증하고, 다양한 응용 사례를 통해 그 효과성을 입증한다.
양자 계산에서 제어 흐름에 대한 오류 정정의 T-복잡도 비용
양자 프로그래밍 추상화에서 제어 흐름은 양자 프로그램의 T-복잡도를 다항식적으로 증가시킬 수 있으며, 이는 양자 알고리즘의 계산 이점을 감소시킬 수 있다.
양자 회로의 타입 기반 합성적 계산
본 논문은 양자 회로를 표현하고 그 속성을 증명하기 위한 타입 이론적 프레임워크를 제안한다. 이는 Coq의 다형성 타입 시스템에서 양자 상태에 대한 커링을 활용하여 복잡한 회로 내에서 양자 게이트를 직접 적용할 수 있게 한다. 또한 렌즈라는 이산적 개념을 도입하여 회로 구조의 조합론과 게이트의 계산 내용을 분리할 수 있다. 이를 통해 하향식으로 양자 회로를 재귀적으로 정의하고 합성적으로 그 정확성을 증명할 수 있다.
현실적이고 단일한 양자 프로그래밍 언어
양자 프로그래밍 언어의 실현 가능성과 단일성
