Implementing a programming language with a dependent type system

Abstract

O objetivo principal desse projeto é discutir sobre as vantagens de sistema de tipos avançados, na área de desenvolvimento de software, através da implementação de uma linguagem de programação com um sistema de tipos dependentes. Isso pode ajudar a melhorar a confiabilidade e segurança do software, permitindo a verificação estática de propriedades arbitrárias sobre o código. O cálculo lambda é expandido com tipos dependentes, o que possibilita a escrita de programas que realizam computações e também permitem a prova da corretude de seu comportamento.

The main goal of this project is to explore the potential benefits of advanced type systems, in software development, through an implementation of a dependently typed programming language. This could help improve the reliability and safety of software by enabling static verification of arbitrary properties about the code. This work consists in an extension of the lambda calculus with dependent types, which allows us to write programs that not only have the ability to perform computations, but whose correctness can also be proven.