Curry-Howard Isomorphism and the Formal Verification of Programs

• Grant number: 25/21977-0
• Support Opportunities: Scholarships in Brazil - Scientific Initiation
• Start date: November 01, 2025
• End date: October 31, 2026
• Field of knowledge: Physical Sciences and Mathematics - Computer Science - Computational Mathematics
• Principal Investigator: Stefano Nardulli
• Grantee: David Batista da Silva
• Host Institution: Centro de Matemática, Computação e Cognição (CMCC). Universidade Federal do ABC (UFABC). Santo André , SP, Brazil
• Associated research grant: 21/05256-0 - Geometric variational problems: existence, regularity and geometrical characterization of the solutions, AP.JP

Abstract

This project aims to explore how Curry-Howard isomorphism (also known as proofs as programs or propositions as types) is applied in formal program verification. To this end, a proof will be developed by constructing the DSA (Digital Signature Algorithm) algorithm in Lean, a dependently typed functional programming language developed by Leonardo de Moura while still working at Microsoft Research. Throughout the proof of the algorithm, we will discuss how Curry-Howard isomorphism allows us to establish a close relationship between functional languages ¿¿and mathematical logic.