Formal-Verification

型理論與 Curry-Howard 同構：命題=型別、證明=程式的深遠和諧