Banca de QUALIFICAÇÃO: BRUNO FRANCISCO XAVIER

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
STUDENT : BRUNO FRANCISCO XAVIER
DATE: 12/04/2022
TIME: 14:00
LOCAL: Google Meets
TITLE:

Linear logic as a framework

KEY WORDS:

Linear Logic; Framework; Cut elimination; Multimodality; Coq

PAGES: 138
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUBÁREA: Teoria da Computação
SPECIALTY: Lógicas e Semântica de Programas
SUMMARY:

The use of linear logic as a logical framework consists of: (1) embed sequents from a given object logic using two predicates that differentiate left-hand formulas from right-hand formulas; and (2) translate the sequent calculus rules of the object logic as theories (clauses) of linear logic. If the set of theories has certain characteristics, we can establish interesting results, such as the admissibility of the cut rule, without the need for a direct proof in the object logic. Using linear logic as a framework to reason about various logical systems, in particular modal systems, and establish suitable translations that meet the characteristics necessary to conclude the admissibility of cut for these systems is the objective of this work. Moreover, we aim at formalizing all the results in a semiautomatic theorem prover. It is a applied research, of a descriptive nature, through a review of studies on the use of linear logic as a framework. This thesis brings also new results for the cut-elimination procedure of linear logic: we present a new proof of cut admissibility directly in the focused system and mechanize such procedure in Coq.

BANKING MEMBERS:
Interno - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interna - 1143603 - ELAINE GOUVEA PIMENTEL
Interno - 1345816 - REGIVAN HUGO NUNES SANTIAGO
Externa à Instituição - GISELLE MACHADO NOGUEIRA REIS