Advanced search
Start date
Betweenand

Genericity in the context of theorem proving: a cloud based proof assistant for flow-based languages

Grant number: 21/01025-3
Support type:Scholarships in Brazil - Doctorate
Effective date (Start): November 01, 2021
Effective date (End): July 31, 2025
Field of knowledge:Humanities - Philosophy - Logic
Principal researcher:Giorgio Venturi
Grantee:Renato Reis Leme
Home Institution: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brazil

Abstract

This project proposes the complete development of a proof assistant focused on diagrammatic reasoning in all its stages, namely: (i) software development (ii) debugging (iii) documentation. Among the main characteristics of this proposal, we highlight the implementation of the generic language paradigm through the notion of homomorphism between graphs, the implementation of a formal language for the specification of tableaux, the creation of a user management system with distinction of profiles, as well as hosting the environment entirely in the cloud, facilitating portability and making the system ideal for distance learning contexts. In addition to the software, we propose to develop the thesis containing an exposition of the formal theory of test assistants (type theory), the philosophical aspects involved in the concept of diagrammatic reasoning, and the complete description of the environment, including the results obtained during debugging phase. (AU)

News published in Agência FAPESP Newsletter about the scholarship:
Articles published in other media outlets (0 total):
More itemsLess items
VEICULO: TITULO (DATA)
VEICULO: TITULO (DATA)

Please report errors in scientific publications list by writing to: cdi@fapesp.br.