This library provides a formalization of fundamental computability concepts, such as termination.
The results are expressed on a simple functional language called PVS0.
| Theorem | Location | PVS Name | Contributors |
|---|
- César Muñoz, NASA, USA
- Andreia Avelar Borges, University of Brasilia, Brazil
- Mauricio Ayala-Rincón, University of Brasilia, Brazil
- Ariane Alves Almeida, University of Brasilia, Brazil
- Thiago Mendonça Ferreira Ramos, University of Brasilia, Brazil
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
