請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/8253
標題: | 形式化驗證零知識證明系統編譯器 From a Dependently Typed Language to ZK-SNARKs Circuits: A Formally Verified Compiler |
作者: | Ruey-Lin Hsu 許瑞麟 |
指導教授: | 鄭振牟(Chen-Mou Cheng) |
關鍵字: | 依值型別程式設計,互動式定理證明器,可驗證計算,形式化驗證,Agda, dependently typed programming,interactive theorem prover,verifiable computation,formal verification,Agda, |
出版年 : | 2020 |
學位: | 碩士 |
摘要: | 本論文提出一個依值型別的可驗證計算編譯器,並證明其可靠性。此編譯器將一個淺層嵌入於 Agda 當中,具有依值型別的領域特定語言轉換成一階限制條件。可靠性是轉換正確性的一個部份,表示如果產生出來的限制條件是可被滿足的,那產生出來的限制條件會是正確的。藉由利用柯里-霍華德對應,我們在互動式定理證明器 Agda 當中建構此編譯器的形式規格以及證明其可靠性。 In this thesis, we will construct and prove the soundness of a dependently typed verifiable computation compiler. The compiler described in this thesis compiles a user program written in a dependently typed shallowly embedded domain specific language in Agda into a set of rank 1 constraints. Soundness is a part of translational correctness that says that if the generated constraints are satisfiable, then the generated constraints are correct. By utilizing the Curry-Howard correspondence, the compiler is formally specified and proved in the interactive theorem prover Agda. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/8253 |
DOI: | 10.6342/NTU202003013 |
全文授權: | 同意授權(全球公開) |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
U0001-1108202022141900.pdf | 663.79 kB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。