About
I am a second-year PhD student supervised by Pablo Barenbaum at the ICC (FCEyN, University of Buenos Aires). I am a member of the LOREL team and my research is supported by a CONICET doctoral fellowship.
My academic background is in Pure Mathematics. I completed my Licenciatura en Ciencias Matemáticas at DM-UBA.
Interests
Computational content of Classical Logic, Linear Logic, Realizability, Proof assistants, Intersection of Algebra and λ-Calculus.Work
Abstract
Linear logic is a resource-conscious logic, where formulae cannot be arbitrarily duplicated or erased, making it a suitable language for modeling resource-sensitive phenomena. Starting from a single-conclusion natural deduction presentation for intuitionistic multiplicative linear logic (IMLL), adding linear negation leads us to the classical law of contraposition. In this setting, classical multiplicative linear logic (MLL) can be recovered simply by introducing a linear modus tollens rule.
We provide a computational interpretation for this inference system through the Curry-Howard correspondence and we present a calculus where the central computational novelty is the necessity of a new operation which we call “contra-substitution”. We then extend these ideas to the full multiplicative-exponential fragment (MELL) and prove that it has the desirable properties: confluence, strong normalization, and subject reduction. Finally, we show how certain well-known term assignments for classical logic embed into our calculus.