| |
| Acadêmico(a): André Ramaciotti da Silva |
| Título: Provador interativo de teoremas com tipos dependentes |
| |
| Abstract: |
| This document presents the specification and implementation of an interactive theorem prover based on a formal language with dependent types. With it, a way in which computers may help in the mathematical development is shown, and the theory of dependent types is introduced to programmers in a simplified language. In more details, the objectives are to specify a language for describing programs and first-order logic theorems and a type system based on the theory of dependent types, to implement a command line interpreter, and to validate programs and first-order logic theorems written in this language. For this, during the development, a formal definition for this language is developed through the Backus-Naur Form (BNF) notation, and a command line interpreter is implemented with the Haskell language and the Parsec library. Finally, all the objectives are reached, although the use of dependent type theory makes the definition of certain types and functions more complex, besides restricting the theorems that can be proved to those with constructive proofs. A comparison is made between the Agda and Coq language, and the language developed by Löh, McBride and Swierstra (2010), showing that Coq’s approach of separating proofs from function definitions makes code more readable. |
| |
|
