Mechanizing focused linear logic in coq

Xavier, Bruno; Vega, Carlos Alberto Olarte; Reis, Giselle; Nigam, Vivek

Mechanizing focused linear logic in coq

Página do item simplificado Estatísticas

dc.contributor.author	Xavier, Bruno
dc.contributor.author	Vega, Carlos Alberto Olarte
dc.contributor.author	Reis, Giselle
dc.contributor.author	Nigam, Vivek
dc.date.accessioned	2020-07-30T17:39:25Z
dc.date.available	2020-07-30T17:39:25Z
dc.date.issued	2018
dc.description.resumo	Linear logic has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. Linear logic's cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. Cut-elimination guarantees that linear logic is consistent and has the so-called sub-formula property. Focusing is a discipline for proof search that was introduced to reduce the search space, but has proved to have more value, as it allows one to specify the shapes of proofs available. This paper formalizes first-order linear logic in Coq and mechanizes the proof of cut-elimination and the completeness of focusing. Moreover, the implemented logic is used to encode an object logic, such as in a linear logical framework, and prove adequacy	pt_BR
dc.identifier.citation	XAVIER, Bruno; OLARTE, Carlos; REIS, Giselle; NIGAM, Vivek. Mechanizing Focused Linear Logic in Coq. Electronic Notes in Theoretical Computer Science, [S.L.], v. 338, p. 219-236, out. 2018. Disponível em: https://www.sciencedirect.com/science/article/pii/S157106611830080X?via%3Dihub. Acesso em: 29 jul. 2020. http://dx.doi.org/10.1016/j.entcs.2018.10.014.	pt_BR
dc.identifier.doi	10.1016/j.entcs.2018.10.014
dc.identifier.issn	1571-0661
dc.identifier.uri	https://repositorio.ufrn.br/jspui/handle/123456789/29755
dc.language	en	pt_BR
dc.publisher	Elsevier	pt_BR
dc.subject	Linear logic	pt_BR
dc.subject	Focusing	pt_BR
dc.subject	Coq	pt_BR
dc.title	Mechanizing focused linear logic in coq	pt_BR
dc.type	article	pt_BR