Skip to content

Latest commit

 

History

History
30 lines (21 loc) · 1.46 KB

index.md

File metadata and controls

30 lines (21 loc) · 1.46 KB
layout title
home
LiVES

LiVES is the Programming Languages, Software Verification and Specification research group of Departament of Computer Science of Federal University of Ouro Preto (UFOP), Minas Gerais, Brazil.

Research themes

Our vision is to use mathematics to understand the nature of computation, and to turn that understanding into the next generation of programming languages and software verification tools.

Through the Curry-Howard correspondence we see mathematics and its foundations as an activity that has an essential programming nature. Guided by the light of computational trinitarianism, our main research tools to achieve better solutions to programming / mathematical problems are:

  • Functional Programming: Using modern programming languages like Haskell, Agda and Coq.

  • Logics: We use non-classical logics as a formal language to specify software requirements.

  • Type theory: We design type systems and its checking / inference algorithms as a tool for checking code and provide better programming abstractions.